def le_sub

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rtools.bend:170

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

170def le_sub(+a: Nat, +c: Nat, +b: Nat, +h: {Nat.is_le(Nat.add(a, c), b) == True{} : Bool}) -> {Nat.is_le(a, Nat.sub(b, c)) == True{} : Bool}:
171  +eb = N.sub_add(b, Nat.add(a, c), h)
172  +r = Nat.sub(b, Nat.add(a, c))
173  +e1 = Equal.trans(Nat, Nat.sub(b, c), Nat.sub(Nat.add(Nat.add(a, c), r), c), Nat.add(a, r), Equal.cong(Nat, Nat, z => Nat.sub(z, c), b, Nat.add(Nat.add(a, c), r), Equal.sym(Nat, Nat.add(Nat.add(a, c), r), b, eb)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(a, c), r), c), Nat.sub(Nat.add(c, Nat.add(a, r)), c), Nat.add(a, r), Equal.cong(Nat, Nat, z => Nat.sub(z, c), Nat.add(Nat.add(a, c), r), Nat.add(c, Nat.add(a, r)), Equal.trans(Nat, Nat.add(Nat.add(a, c), r), Nat.add(Nat.add(c, a), r), Nat.add(c, Nat.add(a, r)), Equal.cong(Nat, Nat, z => Nat.add(z, r), Nat.add(a, c), Nat.add(c, a), NA.add_comm(a, c)), NA.add_assoc(c, a, r))), N.add_sub_cancel(c, Nat.add(a, r))))
174  L.subst(Nat, z => {Nat.is_le(a, z) == True{} : Bool}, Nat.add(a, r), Nat.sub(b, c), Equal.sym(Nat, Nat.sub(b, c), Nat.add(a, r), e1), N.le_add_right(a, r))