proposition: Lemma has_split_eq l: has (fun z => z != 0) l -> exists l1 a l2, [/\ l = l1 ++ a :: l2, a !=0 & all_eq0 l1].
proof: Proof. move/has_split => [l1 [a [l2 [-> pa pb]]]]; exists l1,a,l2; split => //. by apply /allP => x; move /(allP pb); case (x==0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)