def le_add_left

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:331

import Base

331def le_add_left(+a: Nat, +b: Nat, +c: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}:
332  match c:
333    case 0n:
334      e
335    case 1n+r:
336      le_add_left(a, b, r, e)