proposition: Lemma alternate_P (l: seq R): reflect (exists l1 x l2 y l3, [/\ l = l1 ++ x :: l2 ++ (y :: l3), x<0, y> 0 & [/\ all_eq0 l1, all_le0 l2& all_ge0 l3]]) (alternate l).
proof: Proof. apply: (iffP idP); last first. move => [l1 [x [l2 [y [l3 [-> xn yp [l1p l2p l3p]]]]]]]. have h:alternate_1 (l2 ++y :: l3) by apply /alternate_1P; exists l2, y, l3. move: l1p; elim l1; first by rewrite /= xn h. by move => a l' hrec /= /andP [ az] /hrec ->; rewrite lt_neqAle az. elim: l => // a l Hrec /=. rewrite lt_neqAle; case az: (a==0). rewrite andFb => /Hrec [l1 [x [l2 [y [l3 [-> xn yn [l1n l2z l3p]]]]]]]. exists (a :: l1), x, l2, y,l3; split => //; split => //. apply /allP => t; rewrite in_cons; case /orP; last by move/(allP l1n). move /eqP;move/eqP: az => -> -> //. case ane:(a <= 0) => //= /alternate_1P [l1 [x [l2 [-> l1n l2p xp]]]]. by exists [::], a, l1, x,l2; rewrite lt_neqAle az ane. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol