proposition: Lemma schange_index_alternate l: (schange l = 1%N) <-> (alternate l \/ alternate (opp_seq l)).
proof: Proof. have aux0 : (schange l = 1%N) <-> size (schange_index l) = 2%N. rewrite /schange; split; last by move => ->. by case (size (schange_index l)) => // n /= ->. apply:(iff_trans aux0). have aux: forall l, alternate l -> size (schange_index l) = 2%N. move => l0 /alternate_P [l1 [x [l2 [y [l3 [-> xn yp [l1p l2p l3p]]]]]]]. move: (xn); rewrite lt_neqAle => /andP [xnz _]. move: (yp); rewrite lt0r => /andP [ynz _]. have yxn: y * x < 0 by rewrite pmulr_rlt0. have l2p': all_ss x l2 by apply /allP => z/(allP l2p); rewrite nmulr_lge0. have l3p': all_ss y l3 by apply /allP => z/(allP l3p); rewrite pmulr_lge0. move: l3p'; rewrite (schangei_reca l3 ((size l1).+1 + size l2).+1 ynz). by rewrite (schangei_s0n _ xnz l1p) (schangei_recb _ _ yxn l2p') => /eqP->. have p1a: forall a l, a <0 -> all_ss a l -> all_le0 l. by move => a l1 anz h; apply /allP => x /(allP h); rewrite nmulr_lge0. have p1b: forall b l, 0 <b -> all_ss b l -> all_ge0 l. by move => a l1 anz h; apply /allP => x /(allP h); rewrite pmulr_lge0. have px: forall a l, a !=0 -> all_ss a l -> all_ss (-a) (opp_seq l). move => a l1 anz h; apply /allP => x /mapP [y /(allP h) h1 ->]. by rewrite mulrNN. split; last first. by case; move /aux => //; rewrite - schangei_opp. move=> h. have [i [j]]: exists a b, (schange_index l) = [:: a; b]. move: h; set s := (schange_index l); case: s => // a; case => // b. by case => // _; exists a, b. move /schangei_snn => [l1 [a [l2 [lv anz iv pr1 pr2]]]]. move: (schangei_recc anz pr2); move =>[l3 [b [l4 [l2v ban bz l3p [jv]]]]]. move /eqP; rewrite - (schangei_reca _ _ bz) => l4p. move:anz; rewrite neq_lt; case /orP => sa; [left | right];apply /alternate_P. exists l1, a, l3, b, l4; move: ban;rewrite lv l2v (nmulr_llt0 b sa) => sb. split => //;split; [ exact| apply: (p1a _ _ sa l3p)| apply: (p1b _ _ sb l4p)]. exists (opp_seq l1), (-a), (opp_seq l3), (-b), (opp_seq l4); move: ban. rewrite (pmulr_llt0 b sa) => bn. have man: - a < 0 by rewrite oppr_lt0. have mbp: 0 < - b by rewrite oppr_gt0. split => //. by rewrite lv l2v /opp_seq map_cat map_cons map_cat map_cons. split. by apply /allP => x /mapP [y /(allP pr1) /eqP -> ->]; rewrite oppr0 eqxx. by apply (p1a (- a)) => //; apply px => //; move: sa; rewrite lt0r;case /andP. by apply (p1b (- b)) => //; apply px. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol