proposition: Lemma rgcd0p : left_id 0 rgcdp.
proof: Proof. move=> p; rewrite /rgcdp size_poly0 size_poly_gt0 if_neg. case: ifP => /= [_ | nzp]; first by rewrite eqxx. by rewrite polySpred !(rmodp0, nzp) //; case: _.-1 => [|m]; rewrite rmod0p eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)