def prod_le

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/sqrtn.bend:35

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 A

35# u + v <= 2 w gives u v <= w w
36def prod_le(+u: Nat, +v: Nat, +w: Nat, +h: {Nat.is_le(Nat.add(u, v), Nat.add(w, w)) == True{} : Bool}) -> {Nat.is_le(Nat.mul(u, v), Nat.mul(w, w)) == True{} : Bool}:
37  match u v w:
38    case 0n v0 w0:
39      N.zero_le(Nat.mul(w0, w0))
40    case 1n+ +up 0n w0:
41      %Equal.sym(Nat, Nat.mul(1n+up, 0n), 0n, A.mul_zero(1n+up)) : {Nat.is_le(_, Nat.mul(w0, w0)) == True{} : Bool}
42      N.zero_le(Nat.mul(w0, w0))
43    case 1n+ +up 1n+ +vp 0n:
44      Empty.absurd({Nat.is_le(Nat.mul(1n+up, 1n+vp), 0n) == True{} : Bool}, L.false_true(Equal.trans(Bool, False{}, Nat.is_le(Nat.add(1n+up, 1n+vp), 0n), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, 0n), 2n+Nat.add(up, vp), Nat.add(1n+up, 1n+vp), Equal.sym(Nat, Nat.add(1n+up, 1n+vp), 2n+Nat.add(up, vp), add_two(up, vp))), h)))
45    case 1n+ +up 1n+ +vp 1n+ +wp:
46      +h2 = Equal.trans(Bool, Nat.is_le(Nat.add(up, vp), Nat.add(wp, wp)), Nat.is_le(Nat.add(1n+up, 1n+vp), Nat.add(1n+wp, 1n+wp)), True{},
47        Equal.trans(Bool, Nat.is_le(Nat.add(up, vp), Nat.add(wp, wp)), Nat.is_le(2n+Nat.add(up, vp), 2n+Nat.add(wp, wp)), Nat.is_le(Nat.add(1n+up, 1n+vp), Nat.add(1n+wp, 1n+wp)), {==},
48          Equal.trans(Bool, Nat.is_le(2n+Nat.add(up, vp), 2n+Nat.add(wp, wp)), Nat.is_le(Nat.add(1n+up, 1n+vp), 2n+Nat.add(wp, wp)), Nat.is_le(Nat.add(1n+up, 1n+vp), Nat.add(1n+wp, 1n+wp)), Equal.cong(Nat, Bool, z => Nat.is_le(z, 2n+Nat.add(wp, wp)), 2n+Nat.add(up, vp), Nat.add(1n+up, 1n+vp), Equal.sym(Nat, Nat.add(1n+up, 1n+vp), 2n+Nat.add(up, vp), add_two(up, vp))), Equal.cong(Nat, Bool, z => Nat.is_le(Nat.add(1n+up, 1n+vp), z), 2n+Nat.add(wp, wp), Nat.add(1n+wp, 1n+wp), Equal.sym(Nat, Nat.add(1n+wp, 1n+wp), 2n+Nat.add(wp, wp), add_two(wp, wp))))), h)
49      %Equal.sym(Nat, Nat.mul(1n+up, 1n+vp), 1n+Nat.add(Nat.add(up, vp), Nat.mul(up, vp)), succ_mul_succ(up, vp)) : {Nat.is_le(_, Nat.mul(1n+wp, 1n+wp)) == True{} : Bool}
50      %Equal.sym(Nat, Nat.mul(1n+wp, 1n+wp), 1n+Nat.add(Nat.add(wp, wp), Nat.mul(wp, wp)), succ_mul_succ(wp, wp)) : {Nat.is_le(1n+Nat.add(Nat.add(up, vp), Nat.mul(up, vp)), _) == True{} : Bool}
51      le_add2(Nat.add(up, vp), Nat.add(wp, wp), Nat.mul(up, vp), Nat.mul(wp, wp), h2, prod_le(up, vp, wp, h2))