def mul_lt_sq

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64mul.bend:41

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/arith.bend as AR

41# x, y < s gives x * y < s * s
42def mul_lt_sq(+x: Nat, +y: Nat, +s: Nat, +hx: {Nat.is_lt(x, s) == True{} : Bool}, +hy: {Nat.is_lt(y, s) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(x, y), Nat.mul(s, s)) == True{} : Bool}:
43  match s:
44    case 0n:
45      Empty.absurd({Nat.is_lt(Nat.mul(x, y), 0n) == True{} : Bool}, N.lt_zero_absurd(x, hx))
46    case 1n+ +sp:
47      +a1 = AR.mul_le(x, sp, y, N.lt_succ_le(x, sp, hx))
48      +a2 = le_mul_r(sp, y, sp, N.lt_succ_le(y, sp, hy))
49      +a3 = le_mul_r(sp, sp, 1n+sp, N.le_succ(sp))
50      +a4 = N.le_trans(Nat.mul(x, y), Nat.mul(sp, y), Nat.mul(sp, sp), a1, a2)
51      +a5 = N.le_trans(Nat.mul(x, y), Nat.mul(sp, sp), Nat.mul(sp, 1n+sp), a4, a3)
52      N.le_lt_trans(Nat.mul(x, y), Nat.mul(sp, 1n+sp), Nat.add(1n+sp, Nat.mul(sp, 1n+sp)), a5, N.lt_add_r2(0n, 1n+sp, Nat.mul(sp, 1n+sp), {==}))