proposition: Lemma has_split p l: has p l -> exists l1 a l2, [/\ l = l1 ++ a :: l2, p a & all (fun z => ~~(p z)) l1].
proof: Proof. elim:l => // a l Hrec /=; case ha: (p a) => /=. by move => _; exists [::], a, l; split => //. move /Hrec => [l1 [b [l2 [-> pb pc]]]]. by exists (a::l1),b,l2; split => //=; rewrite ha pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol