def lt_add_sub

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64adde.bend:23

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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

23def lt_add_sub(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_lt(a, Nat.sub(c, b)) == True{} : Bool}, +hb: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(1n+Nat.add(a, b), c) == True{} : Bool}:
24  +h1 = N.lt_succ_le_succ(a, Nat.sub(c, b), h)
25  +h2 = Equal.trans(Bool, Nat.is_le(Nat.add(1n+a, b), Nat.add(Nat.sub(c, b), b)), Nat.is_le(1n+a, Nat.sub(c, b)), True{}, FR.le_cancel_r(1n+a, Nat.sub(c, b), b), h1)
26  +ec = Equal.trans(Nat, Nat.add(Nat.sub(c, b), b), Nat.add(b, Nat.sub(c, b)), c, NA.add_comm(Nat.sub(c, b), b), N.sub_add(c, b, hb))
27  L.subst(Nat, z => {Nat.is_le(Nat.add(1n+a, b), z) == True{} : Bool}, Nat.add(Nat.sub(c, b), b), c, ec, h2)