proposition: Lemma divpAC p q : lead_coef p \in GRing.unit -> q %/ d %/ p = q %/ p %/ d.
proof: Proof. by move=> ulcp; rewrite !divp_divl // mulrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)