def w_hi

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

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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/bits.bend as BT

518# w <= 2 p gives w - w / 2 <= p
519def w_hi(+w: Nat, +p: Nat, +hw: {Nat.is_le(w, Nat.double(p)) == True{} : Bool}) -> {Nat.is_le(Nat.sub(w, Nat.div(w, 2n)), p) == True{} : Bool}:
520  +q = Nat.div(w, 2n)
521  +r = Nat.mod(w, 2n)
522  +e = BT.half_eq(w)
523  +e2 = Equal.trans(Nat, w, Nat.add(Nat.double(q), r), Nat.add(q, Nat.add(q, r)), e, Equal.trans(Nat, Nat.add(Nat.double(q), r), Nat.add(Nat.add(q, q), r), Nat.add(q, Nat.add(q, r)), Equal.cong(Nat, Nat, t => Nat.add(t, r), Nat.double(q), Nat.add(q, q), NA.double_self(q)), N.add_assoc(q, q, r)))
524  +es = Equal.trans(Nat, Nat.sub(w, q), Nat.sub(Nat.add(q, Nat.add(q, r)), q), Nat.add(q, r), Equal.cong(Nat, Nat, t => Nat.sub(t, q), w, Nat.add(q, Nat.add(q, r)), e2), N.add_sub_cancel(q, Nat.add(q, r)))
525  +hw2 = L.subst(Nat, z => {Nat.is_le(z, Nat.double(p)) == True{} : Bool}, w, Nat.add(Nat.double(q), r), e, hw)
526  L.subst(Nat, z => {Nat.is_le(z, p) == True{} : Bool}, Nat.add(q, r), Nat.sub(w, q), Equal.sym(Nat, Nat.sub(w, q), Nat.add(q, r), es), w_r(q, r, p, BT.half_rem(w), hw2))