proposition: Lemma has_split_eq_rev l: has (fun z => z != 0) l -> exists l1 a l2, [/\ l = l1 ++ a :: l2, a !=0 & all_eq0 l2].
proof: Proof. have <- : (has (fun z : R => z != 0)) (rev l) = has (fun z : R => z != 0) l. by elim:l => [// | a l hr]; rewrite rev_cons has_rcons /= hr. move/has_split_eq => [l1 [a [l2 [lv pa pb]]]]; exists (rev l2),a,(rev l1). by rewrite -(cat1s a) catA cats1 -rev_cons -rev_cat -lv revK /all_eq0 -all_rev. 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)