def sub_plus

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/inverse.bend:65

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/lemmas/proofs/nat_algebra.bend as A

65# u + t == m for t < m, u = m - t
66def sub_plus(+m: Nat, +t: Nat, +h: {Nat.is_lt(t, m) == True{} : Bool}) -> {Nat.add(Nat.sub(m, t), t) == m : Nat}:
67  Equal.trans(Nat, Nat.add(Nat.sub(m, t), t), Nat.add(t, Nat.sub(m, t)), m, A.add_comm(Nat.sub(m, t), t), N.sub_add(m, t, N.lt_le(t, m, h)))