proposition: Lemma dvd_eqp_divl d p q (dvd_dp : d %| q) (eq_pq : p %= q) : p %/ d %= q %/ d.
proof: Proof. case: (eqVneq q 0) eq_pq=> [->|q_neq0]; first by rewrite eqp0=> /eqP->. have d_neq0: d != 0 by apply: contraTneq dvd_dp=> ->; rewrite dvd0p. move=> eq_pq; rewrite -(@eqp_mul2r d) // !divpK // ?(eqp_dvdr _ eq_pq) //. rewrite (eqp_ltrans (eqp_scale _ _)) ?lc_expn_scalp_neq0 //. by rewrite (eqp_rtrans (eqp_scale _ _)) ?lc_expn_scalp_neq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)