proposition: Lemma eqpfP p q : p %= q -> p = (lead_coef p / lead_coef q) *: q.
proof: Proof. have [->|nz_q] := eqVneq q 0; first by rewrite eqp0 scaler0 => /eqP ->. by apply/IdomainUnit.ucl_eqp_eq; rewrite unitfE lead_coef_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)