proposition: Lemma alternate_1P (l: seq R): reflect (exists l1 x l2, [/\ l = l1 ++ ( x :: l2), all_le0 l1, all_ge0 l2 & x > 0] ) (alternate_1 l).
proof: Proof. apply: (iffP idP). elim:l => [// | a l Hrec /=]; case: (ler0P a) => sa. move => /Hrec [l1 [x [l2 [-> l1n l2p xp]]]]. by exists (a::l1), x, l2 => /=;rewrite sa. by move => h1; exists [::], a, l. move=> [l1 [x [l2 [-> l1n l2p xp]]]]. move: l1 l1n; elim; first by move => _ /=; rewrite xp. by move => a l1' Hrec /= /andP [] ap / Hrec aux;rewrite ltNge ap. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol