proposition: Lemma eqp_rgcd_gcd p q : rgcdp p q %= gcdp p q.
proof: Proof. move: {2}(minn (size p) (size q)) (leqnn (minn (size p) (size q))) => n. elim: n p q => [p q|n ihn p q hs]. rewrite leqn0; case: ltnP => _; rewrite size_poly_eq0; move/eqP->. by rewrite gcd0p rgcd0p eqpxx. by rewrite gcdp0 rgcdp0 eqpxx. have [-> | pn0] := eqVneq p 0; first by rewrite gcd0p rgcd0p eqpxx. have [-> | qn0] := eqVneq q 0; first by rewrite gcdp0 rgcdp0 eqpxx. rewrite gcdpE rgcdpE; case: ltnP hs => sp hs. have e := eqp_rmod_mod q p; apply/eqp_trans/ihn: (eqp_gcdl p e). by rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) ?ltn_modp. have e := eqp_rmod_mod p q; apply/eqp_trans/ihn: (eqp_gcdl q e). by rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) ?ltn_modp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)