proposition: Lemma changes_mulC (R : rcfType) (p : {poly R}) (a : R) : a != 0 -> changes p = changes (a *: p).
proof: Proof. move=> Ha. rewrite mul_polyC_seqmul //=. case: p. elim => [Hs//|b/=]. case => [_ _ |c l IHcl Hs] //=. by rewrite !addn0 !mulr0. rewrite /= in IHcl. rewrite IHcl //= /seqmul. apply/eqP. rewrite eqn_add2r !mulrA (mulrC a) -(mulrA b) -expr2 (mulrC _ (a^+2)) -mulrA eq_sym. by rewrite (@pmulr_rlt0 _ (a ^+2) (b * c)) // 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)