proposition: Lemma poly_nat_poly (t: nat) (q: {poly Word}): size q <= t -> nat_to_poly t (poly_to_nat t q) = q.
proof: Proof. elim: t q => [|t IHt] q H. 1: { rewrite size_poly_leq0 in H. move /eqP in H. by subst. } rewrite /= mod_p_muln_p. rewrite divnMDl ?prime_gt0 // divn_small. 2: { destruct (head_poly q) as [c Hc] => /=. by rewrite -words_p_eq. } rewrite addn0 IHt ?cons_head_tail_poly //. rewrite size_tail_poly. by destruct (size q). 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)