proposition: Lemma all_eq0_seqn0 (l : seq R) : (head 0 (seqn0 l) == 0) = (all_eq0 l).
proof: Proof. elim: l=> [ | a l IH]; first by rewrite eqxx. by rewrite /=; case a0: (a == 0) => //=. 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