proposition: Lemma alternate_1_neq0 (p : {poly R}) : alternate_1 p -> p != 0.
proof: Proof. case/alternate_1P=> l1 [v [l2 [h1]]] _ _ _. by rewrite -nil_poly h1 {h1}; case: l1 => //. 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