proposition: Lemma size_poly_to_nat (t: nat) (q: {poly Word}): poly_to_nat t q < p^t.
proof: Proof. elim: t => [// | t IHt] /= in q*. apply: (@leq_trans (poly_to_nat t (tail_poly q) * p + p)). 2: by rewrite expnSr -mulSnr leq_pmul2r // prime_gt0. case: (head_poly q) => a Ha /=. by rewrite ltn_add2l -words_p_eq. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)