proposition: Lemma mult_nf_fin alpha n: nf alpha -> nf (alpha * T1nat n).
proof: Proof. revert n; induction n. - now rewrite mult_a_0. - cbn; destruct alpha as [|alpha0 np alpha1]. + auto. + destruct alpha0. * intro; eapply nf_coeff_irrelevance; eauto. eapply nf_FS. * intro; eapply nf_coeff_irrelevance; eauto. Unshelve. exact 0. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)