def hi_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64dm.bend:44

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
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR2
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64div.bend as W64D
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA

44# q, bh < 1 + p, p >= 1, lo + hi (1 + p) == q bh: hi + 1 < 1 + p
45def hi_lt(+p: Nat, +q: Nat, +bh: Nat, +lo: Nat, +hi: Nat, +hq: {Nat.is_lt(q, 1n+p) == True{} : Bool}, +hb: {Nat.is_lt(bh, 1n+p) == True{} : Bool}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +e: {Nat.add(lo, Nat.mul(hi, 1n+p)) == Nat.mul(q, bh) : Nat}) -> {Nat.is_lt(Nat.add(hi, 1n), 1n+p) == True{} : Bool}:
46  +h1 = N.le_trans(Nat.mul(q, bh), Nat.mul(p, bh), Nat.mul(p, p), AR2.mul_le(q, p, bh, N.lt_succ_le(q, p, hq)), W64M.le_mul_r(p, bh, p, N.lt_succ_le(bh, p, hb)))
47  +h2 = L.subst(Nat, z => {Nat.is_lt(Nat.mul(p, p), z) == True{} : Bool}, Nat.add(p, Nat.mul(p, p)), Nat.mul(p, 1n+p), Equal.sym(Nat, Nat.mul(p, 1n+p), Nat.add(p, Nat.mul(p, p)), NA.mul_succ(p, p)), L.subst(Nat, z => {Nat.is_lt(Nat.mul(p, p), z) == True{} : Bool}, Nat.add(Nat.mul(p, p), p), Nat.add(p, Nat.mul(p, p)), N.add_comm(Nat.mul(p, p), p), lt_add_pos(Nat.mul(p, p), p, N.lt_le_trans(0n, 1n, p, {==}, hp))))
48  +h3 = L.subst(Nat, z => {Nat.is_le(Nat.mul(hi, 1n+p), z) == True{} : Bool}, Nat.add(lo, Nat.mul(hi, 1n+p)), Nat.mul(q, bh), e, L.subst(Nat, z => {Nat.is_le(Nat.mul(hi, 1n+p), z) == True{} : Bool}, Nat.add(Nat.mul(hi, 1n+p), lo), Nat.add(lo, Nat.mul(hi, 1n+p)), N.add_comm(Nat.mul(hi, 1n+p), lo), N.le_add_right(Nat.mul(hi, 1n+p), lo)))
49  +h4 = W64D.lt_cancel_mul(hi, p, 1n+p, N.le_lt_trans(Nat.mul(hi, 1n+p), Nat.mul(p, p), Nat.mul(p, 1n+p), N.le_trans(Nat.mul(hi, 1n+p), Nat.mul(q, bh), Nat.mul(p, p), h3, h1), h2))
50  L.subst(Nat, z => {Nat.is_lt(z, 1n+p) == True{} : Bool}, 1n+hi, Nat.add(hi, 1n), Equal.sym(Nat, Nat.add(hi, 1n), 1n+hi, WA.plus1(hi)), h4)