proposition: Lemma first_pos_no_change_all_ge0 (l : seq R) : 0 <= head 0 (seqn0 l) -> changes (seqn0 l) = 0%N -> all_ge0 l.
proof: Proof. elim: l=> [ | a l IH] //=; case a0: (a==0)=> /= hsn0. by rewrite le_eqVlt eq_sym a0 /=; apply: IH => //; apply/eqP. case h0: (head 0 (seqn0 l) == 0); move: (h0). rewrite all_eq0_seqn0 hsn0 /= => al0 _. by move: al0; apply: sub_all => x x0; rewrite (eqP x0) lexx. move=> _ /eqP; rewrite hsn0 addn_eq0 /= => /andP [p1]/eqP. apply: IH. have hsn0' : 0 < a by rewrite lt_neqAle eq_sym a0. rewrite -(ler_pmul2l 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