def lt_add_left

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:324

import Base

324def lt_add_left(+a: Nat, +b: Nat, +c: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}:
325  match c:
326    case 0n:
327      e
328    case 1n+r:
329      lt_add_left(a, b, r, e)