def halve2

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

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

92# two remainders later the divisor has at least halved
93def halve2(+b: Nat, +r1: Nat, +r2: Nat, +k: Nat, +hb: {Nat.is_lt(b, Nat.double(k)) == True{} : Bool}, +h21: {Nat.is_lt(r2, r1) == True{} : Bool}, +hs: {Nat.is_le(Nat.add(r2, r1), b) == True{} : Bool}) -> {Nat.is_lt(r2, k) == True{} : Bool}:
94  +a1 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(r2, r1)) == True{} : Bool}, Nat.add(r2, r2), Nat.double(r2), Equal.sym(Nat, Nat.double(r2), Nat.add(r2, r2), NA.double_self(r2)), N.lt_add_left(r2, r1, r2, h21))
95  +a2 = N.lt_le_trans(Nat.double(r2), Nat.add(r2, r1), b, a1, hs)
96  N.bit_double_lt(False{}, r2, k, N.lt_trans(Nat.double(r2), b, Nat.double(k), a2, hb))