def rl_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:1125

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I

1125def rl_v(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +k: Nat, +r: U32) -> {G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, r) == Nat.is_le(Nat.pow(v(r), k), v(n)) : Bool}:
1126  +P = Nat.pow(v(r), k)
1127  Equal.trans(Bool, G.root_le_fin(~U32, ~I.u32_op, ~I.u32_is, n, G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 1n+k, k, r, True{}, (I.u32_op(NM.One{}), True{}))), G.root_le_fin(~U32, ~I.u32_op, ~I.u32_is, n, G.fits(U32, Bool.not(C.fits(32n, P)), of(P))), Nat.is_le(P, v(n)), Equal.cong(Maybe<&2, U32>, Bool, t => G.root_le_fin(~U32, ~I.u32_op, ~I.u32_is, n, t), G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 1n+k, k, r, True{}, (I.u32_op(NM.One{}), True{})), G.fits(U32, Bool.not(C.fits(32n, P)), of(P)), pw_val(r, k, md_init(v(r)))), rlf(K, hK, n, P, C.fits(32n, P), {==}))