proposition: Lemma seqn0_last (l : seq R) : head 0 (seqn0 l) != 0 -> exists l1 x l2, [&& l == l1 ++ x :: l2, x != 0 & all_eq0 l2].
proof: Proof. elim: l => [ | a l IH] /=; first by rewrite eqxx. case a0: (a == 0) => /=. move/IH=> [l1 [x [l2 /andP [p1 p2]]]]; exists (a::l1), x, l2. by rewrite (eqP p1) cat_cons eqxx p2. move=> an0. case h: (all_eq0 l). by exists nil, a, l; rewrite /= an0 h eqxx. move/negbT: h. rewrite -all_eq0_seqn0; move/IH=>[l1 [x [l2 /andP [p1 p2]]]]. by exists (a::l1), x, l2; rewrite (eqP p1) p2 cat_cons eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc