proposition: Lemma first_neg_no_change_all_le0 (l : seq R) : head 0 (seqn0 l) < 0 -> changes (seqn0 l) = 0%N -> all_le0 l.
proof: Proof. elim: l=> [ | a l IH] //=; case a0: (a==0)=> /= hsn0. by rewrite le_eqVlt a0 /=; apply: IH => //; apply/eqP. case h0: (head 0 (seqn0 l) == 0); move: (h0). rewrite all_eq0_seqn0 (ltW hsn0) /= => al0 _. by move: al0; apply: sub_all => x x0; rewrite (eqP x0) lexx. move=> _ /eqP; rewrite (ltW hsn0) addn_eq0 /= => /andP [p1]/eqP. apply: IH. rewrite lt_neqAle h0 /= -(ler_nmul2l hsn0) mulr0. by move: p1; rewrite eqb0 ltNge negbK. 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