proposition: Lemma seqn0_oppr (l : seq R) : seqn0 (map (fun i => -i) l) = map (fun i => -i) (seqn0 l).
proof: Proof. elim: l => [// | a l IH] /=. by rewrite oppr_eq0; case: (a != 0); rewrite /= IH //. 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