def lo_l1

bend-collections-laws-math@1.0.0.0 · proofs/math/u64/u64div.bend:176

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD

176# the top digit of the low limb is below 2^12
177def lo_l1(+one: Nat, +h1: {one == 1n : Nat}, +lo: U32, +c20: U32, +h20: {UD.v(c20) == WD.sc(20n, one) : Nat}, +nz20: {U32.is_zero(c20) == False{} : Bool}) -> {Nat.is_lt(UD.v(U32.div(lo, c20)), WD.sc(12n, one)) == True{} : Bool}:
178  +l1 = UD.v(U32.div(lo, c20))
179  +r1 = UD.v(U32.mod(lo, c20))
180  +e20 = Equal.trans(Nat, Nat.add(WD.sc(20n, l1), r1), Nat.add(Nat.mul(l1, UD.v(c20)), r1), UD.v(lo), Equal.cong(Nat, Nat, z => Nat.add(z, r1), WD.sc(20n, l1), Nat.mul(l1, UD.v(c20)), Equal.sym(Nat, Nat.mul(l1, UD.v(c20)), WD.sc(20n, l1), mul_pow(one, h1, 20n, l1, UD.v(c20), h20))), dm_e(lo, c20, nz20))
181  +le = L.subst(Nat, z => {Nat.is_le(WD.sc(20n, l1), z) == True{} : Bool}, Nat.add(WD.sc(20n, l1), r1), UD.v(lo), e20, N.le_add_right(WD.sc(20n, l1), r1))
182  AR.sc_lt_cancel(20n, l1, WD.sc(12n, one), N.le_lt_trans(WD.sc(20n, l1), UD.v(lo), WD.sc(32n, one), le, UD.vb(one, h1, lo)))