proposition: Lemma changes_seq_incr_0 : forall (s : seq R), (0 < size s)%N -> (increasing s) -> (all_neq0 s) -> ((changes s == 0%N) = (0 < s`_0 * s`_((size s).-1))).
proof: Proof. elim => [ | a] //. case => [_ _ _ /= Ha | b l IH Hsize Hincr Hneq0]. by rewrite /= mulr0 addn0 -expr2 ltxx /= lt_def sqrf_eq0 sqr_ge0 Ha. have/andP [] := Hneq0 => Ha Hblneq0. have/andP [] := Hblneq0 => Hb Hlneq0. have/andP [] := Hincr => Hab Hblincr. rewrite /= addn_eq0 IH //=. apply/idP/idP => [/andP [] H1 H2 | H]; case : (ltrgtP a 0) => Ha2. + by rewrite nmulr_lgt0 // -(@nmulr_rgt0 _ b) // lt_def eq_sym Hb /= -(@nmulr_rge0 _ a) // leNgt -eqb0. - by rewrite pmulr_lgt0 // -(@pmulr_rgt0 _ b) // lt_def Hb /= -(@pmulr_rge0 _ a) // leNgt -eqb0. + by have/eqP := Ha. - have Hbl : ((b :: l)`_(size l) < 0). by rewrite -(nmulr_rgt0 _ Ha2). rewrite eqb0 -leNgt nmulr_rge0 // nmulr_lgt0 //. rewrite le_eqVlt (negbTE Hb) /= andbb (le_lt_trans _ Hbl) //. by apply: (@increasing_is_increasing3 _ Hincr 1%N (size [::a, b & l]).-1). - have Hbl : (0 < (b :: l)`_(size l)). by rewrite -(pmulr_rgt0 _ Ha2). rewrite eqb0 -leNgt pmulr_rge0 // pmulr_lgt0 //. by rewrite le_eqVlt eq_sym (negbTE Hb) /= andbb (lt_le_trans Ha2 Hab). + by have/eqP := Ha. 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)