proposition: Lemma eqp_gdcor p q r : q %= r -> gdcop p q %= gdcop p r.
proof: Proof. move=> eqr; rewrite /gdcop (eqp_size eqr). move: (size r)=> n; elim: n p q r eqr => [|n ihn] p q r; first by rewrite eqpxx. move=> eqr /=; rewrite (eqp_coprimepl p eqr); case: ifP => _ //. exact/ihn/eqp_div/eqp_gcdl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)