proposition: Lemma eqp_eq p q: p %= q -> (lead_coef q) *: p = (lead_coef p) *: q.
proof: Proof. move=> /eqpP [[c1 c2] /= /andP [nz_c1 nz_c2]] eq. have/(congr1 lead_coef) := eq; rewrite !lead_coefZ. move=> eqC; apply/(@mulfI _ c2%:P); rewrite ?polyC_eq0 //. by rewrite !mul_polyC scalerA -eqC mulrC -scalerA eq !scalerA mulrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)