proposition: Lemma rmodpp p : GRing.comm p (lead_coef p)%:P -> rmodp p p = 0.
proof: Proof. move=> hC; rewrite /rmodp unlock; have [-> //|] := eqVneq. rewrite -size_poly_eq0 /redivp_rec; case sp: (size p)=> [|n] // _. rewrite sp ltnn subnn expr0 hC alg_polyC !simp subrr. by case: n sp => [|n] sp; rewrite size_polyC /= eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)