proposition: Lemma modpC p c : c != 0 -> p %% c%:P = 0.
proof: Proof. move=> cn0; rewrite /modp unlock redivp_def /=; case: ifP; rewrite ?rmodpC //. by rewrite scaler0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)