def le_add_cong

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:207

import Base

207def le_add_cong(+c: Nat, +x: Nat, +y: Nat, h: {Nat.is_le(x, y) == True{} : Bool}) ->
208  {Nat.is_le(Nat.add(c, x), Nat.add(c, y)) == True{} : Bool}:
209  match c:
210    case 0n:
211      h
212    case 1n+r:
213      le_add_cong(r, x, y, h)