proposition: Lemma rmod0p p : rmodp 0 p = 0.
proof: Proof. rewrite /rmodp unlock; case: ifP => // Hp; rewrite /redivp_rec !size_poly0. by rewrite polySpred ?Hp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)