proposition: Lemma coef_opp_seqpoly (sp : seqpoly R) (i : nat) : (- sp)%C`_i = - sp`_i.
proof: Proof. have [iltp|pleqi] := ltnP i (size sp). by rewrite (nth_map 0%C). by rewrite !nth_default ?oppr0 ?size_map. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly polydiv) CoqEAL(hrel param refinements poly_op)