def mul_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/scalarops.bend:43

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/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I

43def mul_lt(+a: Nat, +b: Nat, +t: Nat, +ha: {Nat.is_lt(a, t) == True{} : Bool}, +hb: {Nat.is_lt(b, t) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(a, b), Nat.mul(t, t)) == True{} : Bool}:
44  match t:
45    case 0n:
46      Empty.absurd({Nat.is_lt(Nat.mul(a, b), Nat.mul(0n, 0n)) == True{} : Bool}, N.lt_zero_absurd(a, ha))
47    case 1n+ +tp:
48      +s1 = I.le_mul2(a, b, tp, 1n+tp, N.lt_succ_le(a, tp, ha), N.lt_le(b, 1n+tp, hb))
49      +mm = Nat.mul(tp, 1n+tp)
50      +s2 = I.lt_subst_r(mm, Nat.add(mm, 1n+tp), Nat.add(1n+tp, mm), NA.add_comm(mm, 1n+tp), I.lt_add_pos(mm, 1n+tp, {==}))
51      N.le_lt_trans(Nat.mul(a, b), mm, Nat.add(1n+tp, mm), s1, s2)