def low2_le

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

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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

142def low2_le(+Q: Nat, +bp: Nat) -> {Nat.is_le(Nat.mul(1n+C.low(2n, Q), 1n+bp), C.shift(2n, 1n+bp)) == True{} : Bool}:
143  +l = N.lt_succ_le_succ(C.low(2n, Q), 4n, WW.low_lt(2n, Q))
144  +m = NF.mul_le_r(1n+bp, 1n+C.low(2n, Q), 4n, l)
145  +e = Equal.trans(Nat, Nat.mul(1n+bp, 4n), Nat.mul(4n, 1n+bp), C.shift(2n, 1n+bp), NA.mul_comm(1n+bp, 4n), sh_y(2n, 1n+bp))
146  L.subst(Nat, z => {Nat.is_le(Nat.mul(1n+C.low(2n, Q), 1n+bp), z) == True{} : Bool}, Nat.mul(1n+bp, 4n), C.shift(2n, 1n+bp), e, L.subst(Nat, z => {Nat.is_le(z, Nat.mul(1n+bp, 4n)) == True{} : Bool}, Nat.mul(1n+bp, 1n+C.low(2n, Q)), Nat.mul(1n+C.low(2n, Q), 1n+bp), NA.mul_comm(1n+bp, 1n+C.low(2n, Q)), m))