def iq_lt

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

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
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

148# e < b
149def iq_lt(+bp: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, 1n+bp), r2) == C.shift(64n, R) : Nat}, +hr2: {Nat.is_lt(r2, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp) == True{} : Bool}:
150  +E = Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2)
151  +l1 = Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp)), Nat.is_lt(r2, 1n+bp), True{}, WW.lt_cancel_l(Nat.mul(C.low(2n, Q), 1n+bp), r2, 1n+bp), hr2)
152  +e1 = Equal.trans(Nat, Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), Nat.add(1n+bp, Nat.mul(C.low(2n, Q), 1n+bp)), Nat.mul(1n+C.low(2n, Q), 1n+bp), NA.add_comm(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), {==})
153  +l2 = N.lt_le_trans(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), C.shift(2n, 1n+bp), l1, L.subst(Nat, z => {Nat.is_le(z, C.shift(2n, 1n+bp)) == True{} : Bool}, Nat.mul(1n+C.low(2n, Q), 1n+bp), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), Equal.sym(Nat, Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), Nat.mul(1n+C.low(2n, Q), 1n+bp), e1), low2_le(Q, bp)))
154  +l3 = L.subst(Nat, z => {Nat.is_lt(z, C.shift(2n, 1n+bp)) == True{} : Bool}, Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), Equal.sym(Nat, C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), iq_eps(1n+bp, R, Q, r2, hQ)), l2)
155  Equal.trans(Bool, Nat.is_lt(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp), Nat.is_lt(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), C.shift(2n, 1n+bp)), True{}, Equal.sym(Bool, Nat.is_lt(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), C.shift(2n, 1n+bp)), Nat.is_lt(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp), lt_sh(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp)), l3)