proposition: Lemma changes_decomp_sizegt2 : forall (s : seq R), (all_neq0 s) -> (2 < size s)%N -> changes s = ((s`_0 * s`_1 < 0)%R + (changes (mid s))%R + (s`_((size s).-2) * s`_((size s).-1) < 0)%R)%N.
proof: Proof. case=> [|a [| b l]] //. elim: l a b => [ |c l] //. case: l c => [c _ a b Habcneq0 _| d l c IHdl a b /andP [] Ha Hneq0 Hsize ]. by rewrite /= !mulr0 !ltxx !addn0. have H1 : (changes [:: a, b, c, d & l] = ((a * b < 0)%R + changes [:: b, c, d & l])%N). by done. rewrite H1 (IHdl b c) // -addnA -addnA addnC (@addnC (a * b < 0)%R). apply/eqP. rewrite eqn_add2r addnA eqn_add2r (@mid_cons _ a). have H2 : (size [:: b, c, d & l]).-1 = size [::c, d & l]. by done. by rewrite H2 (@changes_take _ b c). 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)