proposition: Lemma changes_size3 : forall (s : seq R), (all_neq0 s) -> (size s = 3)%N -> (s`_0 < 0) -> (0 < s`_2) -> changes s = 1%N.
proof: Proof. case => [ | a [| b [| c]]] //. case => [Hallneq Hsize Ha Hc | ] //=. rewrite mulr0 ltxx !addn0. case : (ltrP (a * b) 0) => Hab. rewrite addnC addn1; apply: eq_S. apply/eqP. by rewrite eqb0 -leNgt pmulr_lge0 // -(@nmulr_lle0 _ a b) // ltW // mulrC. apply/eqP. rewrite add0n eqb1 pmulr_llt0 // -(@nmulr_rgt0 _ a) // lt_def Hab andbT. move/and3P : Hallneq => [] Ha2 Hb2 Hc2. by rewrite mulf_neq0. 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)