def root_le_ok

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/roots.bend:54

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/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as R
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend as LC

54# root_le(n, k, r) is r^k <= n
55def root_le_ok(+n: Nat, +k: Nat, +r: Nat) -> {M.root_le(n, k, r) == Nat.is_le(Nat.pow(r, k), n) : Bool}:
56  match k r:
57    case 0n r0:
58      {==}
59    case 1n+ +kp 0n:
60      Equal.sym(Bool, Nat.is_le(0n, n), True{}, N.zero_le(n))
61    case 1n+ +kp 1n+ +rp:
62      +c = pow_le_case(kp, rp, 1n, n, Nat.is_le(1n, Nat.div(n, 1n+rp)), R.le_div(rp, 1n, n))
63      %Equal.sym(Nat, Nat.pow(1n+rp, 1n+kp), Nat.mul(Nat.mul(1n, 1n+rp), Nat.pow(1n+rp, kp)), Equal.cong(Nat, Nat, z => Nat.mul(z, Nat.pow(1n+rp, kp)), 1n+rp, Nat.mul(1n, 1n+rp), Equal.sym(Nat, Nat.mul(1n, 1n+rp), 1n+rp, LC.one_mul(1n+rp)))) : {M.root_le(n, 1n+kp, 1n+rp) == Nat.is_le(_, n) : Bool}
64      c