proposition: Lemma eqp_trans : transitive (@eqp R).
proof: Proof. move=> p q r; case/andP=> Dp pD; case/andP=> Dq qD. by rewrite /eqp (dvdp_trans Dp) // (dvdp_trans qD). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)