def half_below

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/natfuel.bend:147

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/bits.bend as BT

147# div(n, 2) < p when n < 2p
148def half_below(+n: Nat, +p: Nat, +h: {Nat.is_lt(n, Nat.double(p)) == True{} : Bool}) -> {Nat.is_lt(Nat.div(n, 2n), p) == True{} : Bool}:
149  +e = BT.half_eq(n)
150  +le = L.subst(Nat, z => {Nat.is_le(Nat.double(Nat.div(n, 2n)), z) == True{} : Bool}, Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)), n, Equal.sym(Nat, n, Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)), e), N.le_add_right(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)))
151  N.bit_double_lt(False{}, Nat.div(n, 2n), p, N.le_lt_trans(Nat.double(Nat.div(n, 2n)), n, Nat.double(p), le, h))