def le_add_cong

bendtorch-core@0.1.0.0 · src/tensor/contracts/build_facts.bend:95

import Base

95def le_add_cong(+c: Nat, +x: Nat, +y: Nat, h: {Nat.is_le(x, y) == True{} : Bool}) ->
96  {Nat.is_le(Nat.add(c, x), Nat.add(c, y)) == True{} : Bool}:
97  match c:
98    case 0n:
99      h
100    case 1n+r:
101      le_add_cong(r, x, y, h)