proposition: Lemma changes_nseq : forall (s : seq R) (a : R), a != 0 -> changes (seqmul (nseq (size s) a) s) = changes s.
proof: Proof. elim => [ | c l IHl a Ha] //. case : l IHl => [IH |b l IHbl ] //. by rewrite /= !mulr0 addn0. have -> : (changes [::c, b & l]) = ((c * b < 0)%R + changes [:: b & l])%N. by []. rewrite -(IHbl a) //. suff : ((a * c) * (a * b) < 0) = (c * b < 0) by move=> <-. rewrite (mulrC a b) -mulrA (mulrC a) -!mulrA -expr2 mulrA. by rewrite pmulr_llt0 // exprn_even_gt0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)