def is_eq_add

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sh.bend:350

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

350def is_eq_add(+l: Nat, +s: Nat) -> {Nat.is_eq(s, Nat.add(l, s)) == Nat.is_eq(l, 0n) : Bool}:
351  match l:
352    case 0n:
353      N.is_eq_refl(s)
354    case 1n+ +lp:
355      +h = N.le_lt_trans(s, Nat.add(lp, s), 1n+Nat.add(lp, s), L.subst(Nat, z => {Nat.is_le(s, z) == True{} : Bool}, Nat.add(s, lp), Nat.add(lp, s), N.add_comm(s, lp), N.le_add_right(s, lp)), N.lt_succ(Nat.add(lp, s)))
356      N.is_eq_lt(s, 1n+Nat.add(lp, s), h)