def dpos

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64est.bend:181

import Base
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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD

181# a divisor at most the high word: the high quotient word is nonzero
182def dpos(+hi: U32, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}, +bp: Nat, +hb: {v(d) == 1n+bp : Nat}, +hle: {Nat.is_le(1n+bp, v(hi)) == True{} : Bool}) -> {U32.is_zero(U32.div(hi, d)) == False{} : Bool}:
183  +q = Nat.div(v(hi), 1n+bp)
184  +e1 = Equal.trans(Nat, v(U32.div(hi, d)), Nat.div(v(hi), v(d)), q, UD.div_nat(hi, d, hd), Equal.cong(Nat, Nat, z => Nat.div(v(hi), z), v(d), 1n+bp, hb))
185  +hm = L.subst(Nat, z => {Nat.is_le(z, v(hi)) == True{} : Bool}, 1n+bp, Nat.mul(1n, 1n+bp), Equal.sym(Nat, Nat.mul(1n, 1n+bp), 1n+bp, N.add_zero(1n+bp)), hle)
186  +hq1 = Equal.trans(Bool, Nat.is_le(1n, q), Nat.is_le(Nat.mul(1n, 1n+bp), v(hi)), True{}, NR.le_div(bp, 1n, v(hi)), hm)
187  Equal.trans(Bool, U32.is_zero(U32.div(hi, d)), Nat.is_eq(v(U32.div(hi, d)), 0n), False{}, LW.zero_nat(U32.div(hi, d)), Equal.trans(Bool, Nat.is_eq(v(U32.div(hi, d)), 0n), Nat.is_eq(q, 0n), False{}, Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), v(U32.div(hi, d)), q, e1), ne0(q, hq1)))