proposition: Lemma eqp_rgdco_gdco q p : rgdcop q p %= gdcop q p.
proof: Proof. rewrite /rgdcop /gdcop; move: (size p)=> n. elim: n p q {1 3}p {1 3}q (eqpxx p) (eqpxx q) => [|n ihn] p q s t /= sp tq. case: (eqVneq t 0) tq => [-> | nt0 etq]. by rewrite eqp_sym eqp0 => ->; rewrite eqpxx. by case: (eqVneq q 0) etq nt0 => [->|]; rewrite ?eqpxx // eqp0 => ->. rewrite rcoprimep_coprimep (eqp_coprimepl t sp) (eqp_coprimepr p tq). case: ifP=> // _; apply: ihn => //; apply: eqp_trans (eqp_rdiv_div _ _) _. by apply: eqp_div => //; apply: eqp_trans (eqp_rgcd_gcd _ _) _; apply: eqp_gcd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)