def half_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addp.bend:39

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

39def half_lt(+k: Nat, +t: Nat, +h: {Nat.is_lt(Nat.double(k), Nat.double(t)) == True{} : Bool}) -> {Nat.is_lt(k, t) == True{} : Bool}:
40  Equal.trans(Bool, Nat.is_lt(k, t), Nat.is_lt(Nat.double(k), Nat.double(t)), True{}, Equal.cong(Cmp, Bool, c => Cmp.is_lt(c), Nat.cmp(k, t), Nat.cmp(Nat.double(k), Nat.double(t)), Equal.sym(Cmp, Nat.cmp(Nat.double(k), Nat.double(t)), Nat.cmp(k, t), NC.cmp_dbl(k, t))), h)