proposition: Lemma changes_take : forall (s : seq R) (a b : R), (s != [::]) -> (all_neq0 [::a, b & s]) -> (changes (take (size (b :: s)) ([::a, b & s])) = ((a * b < 0)%R + changes (take (size s) (b :: s)))%N).
proof: Proof. by case. 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)