proposition: Lemma changes_seq_incr : forall (s : seq R), (increasing s) -> (all_neq0 s) -> (changes s == 1%N) || (changes s == 0%N).
proof: Proof. case=> [ |a ] //. case => [_ Ha |b l Hincr Hneq0] //. apply/orP; right. rewrite changes_seq_incr_0 //= -expr2 lt_def. move/andP : Ha; case => Ha _. by rewrite sqrf_eq0 Ha /= sqr_ge0. have/andP [] := Hneq0 => Ha Hblneq0. have/andP [] := Hincr => Hab Hblincr. have Hlast := ((all_neq0P [::a, b & l] Hneq0) ((size [::a, b & l]).-1) (leqnn _)). case : (ltrgtP 0 (a * ([::a, b & l]`_(size [::a, b & l]).-1))) => H. + apply/orP; right. by rewrite changes_seq_incr_0. - apply/orP; left. rewrite changes_seq_incr_1 //=. have H2 := (@increasing_is_increasing3 _ Hincr 0%N (size [:: a, b & l]).-1). case: (ltrgtP a 0) => Ha2 /=. by rewrite -(nmulr_rlt0 _ Ha2). rewrite -(lt_asym 0 [:: a, b & l]`_(size [::a, b & l]).-1). apply/andP; split. by rewrite (lt_le_trans Ha2) // H2. by rewrite -(pmulr_rlt0 _ Ha2). by have/eqP := Ha. + move/eqP : H; rewrite eq_sym => /eqP H. by have/eqP := (mulf_neq0 Ha Hlast). 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)