def iroot_k_ok

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

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

239def iroot_k_ok(+n: Nat, +kp: Nat) -> root_ok(n, 1n+kp, M.iroot_k(n, 1n+kp)):
240  match kp:
241    case 0n:
242      (Equal.trans(Bool, M.root_le(n, 1n, n), Nat.is_le(Nat.mul(n, 1n), n), True{}, root_le_ok(n, 1n, n), Equal.trans(Bool, Nat.is_le(Nat.mul(n, 1n), n), Nat.is_le(n, n), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, n), Nat.mul(n, 1n), n, A.mul_one(n)), N.le_refl(n))),
243       Equal.trans(Bool, M.root_le(n, 1n, 1n+n), Nat.is_le(Nat.mul(1n+n, 1n), n), False{}, root_le_ok(n, 1n, 1n+n), Equal.trans(Bool, Nat.is_le(Nat.mul(1n+n, 1n), n), Nat.is_le(1n+n, n), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, n), Nat.mul(1n+n, 1n), 1n+n, A.mul_one(1n+n)), N.lt_not_le(n, 1n+n, N.lt_succ(n)))))
244    case 1n+ +kq:
245      root_top(n, 1n+kq)