def dbl_le_mul

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/natfuel.bend:317

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

317def dbl_le_mul(+p: Nat, +bq: Nat) -> {Nat.is_le(Nat.double(p), Nat.mul(p, 2n+bq)) == True{} : Bool}:
318  +r = Nat.add(p, Nat.add(p, Nat.mul(p, bq)))
319  +em = Equal.trans(Nat, Nat.mul(p, 2n+bq), Nat.add(p, Nat.mul(p, 1n+bq)), r, NA.mul_succ(p, 1n+bq), Equal.cong(Nat, Nat, t => Nat.add(p, t), Nat.mul(p, 1n+bq), Nat.add(p, Nat.mul(p, bq)), NA.mul_succ(p, bq)))
320  +h0 = N.le_add_left(p, Nat.add(p, Nat.mul(p, bq)), p, N.le_add_right(p, Nat.mul(p, bq)))
321  +h1 = L.subst(Nat, z => {Nat.is_le(z, r) == True{} : Bool}, Nat.add(p, p), Nat.double(p), Equal.sym(Nat, Nat.double(p), Nat.add(p, p), NA.double_self(p)), h0)
322  L.subst(Nat, z => {Nat.is_le(Nat.double(p), z) == True{} : Bool}, r, Nat.mul(p, 2n+bq), Equal.sym(Nat, Nat.mul(p, 2n+bq), r, em), h1)