proposition: Lemma nonneg_changes0 (s : seq R) : nonneg s -> changes s = 0%N.
proof: Proof. elim: s => [ |a ] //. case=> [_ _ |b l IHbl /andP [] Ha Hblnonneg]. by rewrite /= mulr0 addn0 ltxx. have /andP[Hb Hlnonneg] := Hblnonneg. apply/eqP; rewrite addn_eq0 eqb0 -leNgt mulr_ge0 //=. apply/eqP; by apply: IHbl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol