proposition: Lemma monomial_free n (l : nat -> R): \sum_(i < n) l i *: 'X ^+i == 0 -> forall i, (i < n)%N -> l i = 0.
proof: Proof. elim:n => [ | n IH] /=; first by move=> _ i; rewrite ltn0. rewrite big_ord_recr /=. case r : (l n == 0). rewrite (eqP r) scale0r addr0; move/IH=>{IH} II i. rewrite ltnS leq_eqVlt => /predU1P[->|]. exact/eqP. exact: II. rewrite addr_eq0 => abs. case/negP: (negbT (ltnn n)). rewrite [X in (X <= _)%N](_ : _ = size (l n *: 'X^n)); last first. by rewrite -mul_polyC size_Cmul ?r // size_polyXn. rewrite -size_opp -(eqP abs) size_weighted_sum_leq //. by move=> [i ci]; rewrite /= size_polyXn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc