proposition: Lemma mulKp p q : q != 0 -> q * p %/ q = lead_coef q ^+ scalp (p * q) q *: p.
proof: Proof. by move=> nzq; rewrite mulrC; apply: mulpK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)