proposition: Lemma modp0 p : p %% 0 = p.
proof: Proof. rewrite /modp unlock redivp_def; case: ifP; rewrite rmodp0 //= lead_coef0. by rewrite unitr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)