proposition: Lemma eqp_gdcol p q r : q %= r -> gdcop q p %= gdcop r p.
proof: Proof. move=> eqr; rewrite /gdcop; move: (size p)=> n. elim: n p q r eqr {1 3}p (eqpxx p) => [|n ihn] p q r eqr s esp /=. case: (eqVneq q 0) eqr => [-> | nq0 eqr] /=. by rewrite eqp_sym eqp0 => ->; rewrite eqpxx. by case: (eqVneq r 0) eqr nq0 => [->|]; rewrite ?eqpxx // eqp0 => ->. rewrite (eqp_coprimepr _ eqr) (eqp_coprimepl _ esp); case: ifP=> _ //. exact/ihn/eqp_div/eqp_gcd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)