proposition: Lemma ucl_eqp_eq p q : lead_coef q \is a GRing.unit -> p %= q -> p = (lead_coef p / lead_coef q) *: q.
proof: Proof. move=> ulcq /eqp_eq; move/(congr1 ( *:%R (lead_coef q)^-1 )). by rewrite !scalerA mulrC divrr // scale1r mulrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)