proposition: Lemma changes_decomp_size2 : forall (s : seq R), (all_neq0 s) -> (size s == 2)%N -> changes s = (s`_0 * s`_1 < 0)%R.
proof: Proof. case => [ |a [| b [_ _ |]]] //. by rewrite /= mulr0 ltxx !addn0. 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)