proposition: Lemma changes_seq_incr_1 : forall (s : seq R), (1%N < size s)%N -> (increasing s) -> (all_neq0 s) -> ((changes s) == 1%N) = (s`_0 < 0) && (0 < s`_((size s).-1)).
proof: Proof. elim=> [ |a ] //. case=> [_ _ _ _ | b] //. case=> [_ _ /andP [] Hab _ /and3P [] Ha Hb _ |c l IH Hsize Hincr Hneq0] //=. rewrite mulr0 addn0 ltxx /= addn0 eqb1. case: (ltrP a 0) => Ha2 /=; first by rewrite nmulr_rlt0. by rewrite ltNge mulr_ge0 // (le_trans Ha2). have/andP [] := Hneq0 => Ha Hbclneq0. have/andP [] := Hbclneq0 => Hb Hclneq0. have/andP [] := Hclneq0 => Hc Hlneq0. have/andP [] := Hincr => Hab Hbclincr. have/andP [] := Hbclincr => Hbc Hclincr. apply/idP/idP; case : (ltrP (a * b) 0) => Hab2 /=. + case : (ltrgtP a 0) => Ha2 H /=. have Hb2 : (0 < b). rewrite -(nmulr_rlt0 _ Ha2) //. rewrite (lt_le_trans Hb2) //. by apply: (@increasing_is_increasing3 _ Hincr 1%N (size [::a, b, c & l]).-1). rewrite -(lt_asym 0 b); apply/andP; split. by rewrite (lt_le_trans _ Hab). by rewrite -(pmulr_rlt0 _ Ha2). by have/eqP := Ha. - rewrite add0n IH //. case/andP => /= Hb2 Hbl; apply/andP; split => //. by rewrite (le_lt_trans _ Hb2). + case/andP => H1 H2. rewrite addnC addn1. apply/eqP; apply: eq_S; apply/eqP. by rewrite (changes_seq_incr_0 (s:=[::b, c & l])) //= pmulr_rgt0 // -(nmulr_rlt0 _ H1). - case/andP => H1 H2. rewrite add0n IH //. apply/andP; split => //=. rewrite -(nmulr_rgt0 _ H1) lt_def. apply/andP; split => //. by apply: 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)