proposition: Lemma rmodpC p c : c != 0 -> rmodp p c%:P = 0.
proof: Proof. move=> Hc; apply/eqP; rewrite -size_poly_leq0 -ltnS. have -> : 1%N = nat_of_bool (c != 0) by rewrite Hc. by rewrite -size_polyC ltn_rmodp polyC_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)