proposition: Lemma rgcdp0 : right_id 0 rgcdp.
proof: Proof. move=> p; have:= rgcd0p p; rewrite /rgcdp size_poly0 size_poly_gt0. by case: eqVneq => p0; rewrite ?(eqxx, p0) //= eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)