proposition: Lemma eqpP m n : reflect (exists2 c12, (c12.1 != 0) && (c12.2 != 0) & c12.1 *: m = c12.2 *: n) (m %= n).
proof: Proof. apply: (iffP idP) => [| [[c1 c2]/andP[nz_c1 nz_c2 eq_cmn]]]; last first. rewrite /eqp (@eq_dvdp c2 c1%:P) -?eq_cmn ?mul_polyC // (@eq_dvdp c1 c2%:P) //. by rewrite eq_cmn mul_polyC. case: (eqVneq m 0) => [-> /andP [/dvd0pP -> _] | m_nz]. by exists (1, 1); rewrite ?scaler0 // oner_eq0. case: (eqVneq n 0) => [-> /andP [_ /dvd0pP ->] | n_nz /andP []]. by exists (1, 1); rewrite ?scaler0 // oner_eq0. rewrite !dvdp_eq; set c1 := _ ^+ _; set c2 := _ ^+ _. set q1 := _ %/ _; set q2 := _ %/ _; move/eqP => Hq1 /eqP Hq2; have Hc1 : c1 != 0 by rewrite expf_eq0 lead_coef_eq0 negb_and m_nz orbT. have Hc2 : c2 != 0 by rewrite expf_eq0 lead_coef_eq0 negb_and n_nz orbT. have def_q12: q1 * q2 = (c1 * c2)%:P. apply: (mulIf m_nz); rewrite mulrAC mulrC -Hq1 -scalerAr -Hq2 scalerA. by rewrite -mul_polyC. have: q1 * q2 != 0 by rewrite def_q12 -size_poly_eq0 size_polyC mulf_neq0. rewrite mulf_eq0; case/norP=> nz_q1 nz_q2. have: size q2 <= 1. have:= size_mul nz_q1 nz_q2; rewrite def_q12 size_polyC mulf_neq0 //=. by rewrite polySpred // => ->; rewrite leq_addl. rewrite leq_eqVlt ltnS size_poly_leq0 (negPf nz_q2) orbF. case/size_poly1P=> c cn0 cqe; exists (c2, c); first by rewrite Hc2. by rewrite Hq2 -mul_polyC -cqe. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)