proposition: Lemma modpN p : (- p) %% d = - (p %% d).
proof: Proof. by rewrite -mulN1r -[RHS]mulN1r -polyCN !mul_polyC modpZl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)