def le_add_cong

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:117

import Base

117def le_add_cong(+c: Nat, +x: Nat, +y: Nat, h: {Nat.is_le(x, y) == True{} : Bool}) ->
118  {Nat.is_le(Nat.add(c, x), Nat.add(c, y)) == True{} : Bool}:
119  match c:
120    case 0n:
121      h
122    case 1n+p:
123      le_add_cong(p, x, y, h)