def sub_lt_of

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divv.bend:51

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/math/typed/width.bend as WW

51# b <= a and a < 2 b give a - b < b
52def sub_lt_of(+a: Nat, +b: Nat, +hle: {Nat.is_le(b, a) == True{} : Bool}, +h: {Nat.is_lt(a, Nat.add(b, b)) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a, b), b) == True{} : Bool}:
53  +e = N.sub_add(a, b, hle)
54  +h2 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(b, b)) == True{} : Bool}, a, Nat.add(b, Nat.sub(a, b)), Equal.sym(Nat, Nat.add(b, Nat.sub(a, b)), a, e), h)
55  Equal.trans(Bool, Nat.is_lt(Nat.sub(a, b), b), Nat.is_lt(Nat.add(b, Nat.sub(a, b)), Nat.add(b, b)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(b, Nat.sub(a, b)), Nat.add(b, b)), Nat.is_lt(Nat.sub(a, b), b), WW.lt_cancel_l(b, Nat.sub(a, b), b)), h2)