proposition: Lemma changes_oppr (l : seq R) : changes [seq - x | x <- l] = changes l.
proof: Proof. elim: l => [// | x [ | y l] IH] /=; first by rewrite !mulr0. rewrite mulrNN; congr (_ + _)%N; exact: 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