def iq_le

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divn.bend:129

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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

129# h * b <= (a - b) * 2^62
130def iq_le(+B: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, B), r2) == C.shift(64n, R) : Nat}) -> {Nat.is_le(Nat.mul(C.high(2n, Q), B), C.shift(62n, R)) == True{} : Bool}:
131  +p = iq_parts(B, R, Q, r2, hQ)
132  +l = L.subst(Nat, z => {Nat.is_le(C.shift(2n, Nat.mul(C.high(2n, Q), B)), z) == True{} : Bool}, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), C.shift(2n, C.shift(62n, R)), p, N.le_add_right(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)))
133  Equal.trans(Bool, Nat.is_le(Nat.mul(C.high(2n, Q), B), C.shift(62n, R)), Nat.is_le(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, C.shift(62n, R))), True{}, Equal.sym(Bool, Nat.is_le(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, C.shift(62n, R))), Nat.is_le(Nat.mul(C.high(2n, Q), B), C.shift(62n, R)), le_sh(2n, Nat.mul(C.high(2n, Q), B), C.shift(62n, R))), l)