def lt2x

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

82def lt2x(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +m: Nat, +hn: {C.fits(53n, n) == True{} : Bool}, +hm: {C.fits(52n, m) == False{} : Bool}) -> {Nat.is_lt(n, Nat.add(m, m)) == True{} : Bool}:
83  N.lt_le_trans(n, C.shift(53n, one), Nat.add(m, m), hi53(one, h1, n, hn), dbl53(one, h1, m, hm))