def le_div_g

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/arith.bend:70

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 A

70def le_div_g(+x: Nat, +q: Nat, +bp: Nat, +r: Nat, +hr: {Nat.is_lt(r, 1n+bp) == True{} : Bool}) -> {Nat.is_le(x, q) == Nat.is_le(Nat.mul(x, 1n+bp), Nat.add(Nat.mul(q, 1n+bp), r)) : Bool}:
71  match x q:
72    case 0n q0:
73      %Equal.sym(Bool, Nat.is_le(0n, q0), True{}, N.zero_le(q0)) : {_ == Nat.is_le(0n, Nat.add(Nat.mul(q0, 1n+bp), r)) : Bool}
74      Equal.sym(Bool, Nat.is_le(0n, Nat.add(Nat.mul(q0, 1n+bp), r)), True{}, N.zero_le(Nat.add(Nat.mul(q0, 1n+bp), r)))
75    case 1n+ +xp 0n:
76      Equal.sym(Bool, Nat.is_le(Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), r), False{}, N.lt_not_le(r, Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), N.lt_le_trans(r, 1n+bp, Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), hr, N.le_add_right(1n+bp, Nat.mul(xp, 1n+bp)))))
77    case 1n+ +xp 1n+ +qp:
78      %Equal.sym(Nat, Nat.add(Nat.add(1n+bp, Nat.mul(qp, 1n+bp)), r), Nat.add(1n+bp, Nat.add(Nat.mul(qp, 1n+bp), r)), A.add_assoc(1n+bp, Nat.mul(qp, 1n+bp), r)) : {Nat.is_le(xp, qp) == Nat.is_le(Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), _) : Bool}
79      %Equal.sym(Bool, Nat.is_le(Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), Nat.add(1n+bp, Nat.add(Nat.mul(qp, 1n+bp), r))), Nat.is_le(Nat.mul(xp, 1n+bp), Nat.add(Nat.mul(qp, 1n+bp), r)), le_add_cancel(1n+bp, Nat.mul(xp, 1n+bp), Nat.add(Nat.mul(qp, 1n+bp), r))) : {Nat.is_le(xp, qp) == _ : Bool}
80      le_div_g(xp, qp, bp, r, hr)