proposition: Lemma changes_mult : forall (s c : seq R), all_pos c -> (size s = size c) -> changes (seqmul s c) = changes s.
proof: Proof. elim=> [c Hc Hsize |a1 s IHs]. by rewrite seqmul0. case=> [ |b1 l Hblpos Hsize] //. rewrite seqmul_cons /=. case: s IHs Hsize => [IH Hsize|a2 s IHa2s Hsize]. by rewrite seqmul0 /= !addn0 !mulr0. case : l Hblpos Hsize => [ | b2 l /andP [] Hb1 Hb2lpos Hsize] //. have/andP [Hb2 Hlpos] := Hb2lpos. rewrite !seqmul_cons -(@IHa2s (b2::l)) //. by rewrite seqmul_cons -(@pmulr_llt0 _ b1 (a1 * head 0 (a2 :: s ))) // -(@mulrA _ a1 _ b1) (@mulrC _ (head 0 (a2::s)) b1) (@mulrA _ a1 b1 _) -(@pmulr_llt0 _ b2 (a1 * b1 * head 0 (a2 :: s ))) // -!mulrA (@mulrC _ _ b2). by apply: eq_add_S. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)