def cmp_add

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natcmp.bend:43

import Base

43def cmp_add(+d: Nat, +a: Nat, +b: Nat) -> {Nat.cmp(Nat.add(d, a), Nat.add(d, b)) == Nat.cmp(a, b) : Cmp}:
44  match d:
45    case 0n:
46      {==}
47    case 1n+ +dp:
48      cmp_add(dp, a, b)