proposition: Lemma ulc_eqpP p q : lead_coef q \is a GRing.unit -> reflect (exists2 c : R, c != 0 & p = c *: q) (p %= q).
proof: Proof. have [->|] := eqVneq (lead_coef q) 0; first by rewrite unitr0. rewrite lead_coef_eq0 => nz_q ulcq; apply: (iffP idP). have [->|nz_p] := eqVneq p 0; first by rewrite eqp_sym eqp0 (negPf nz_q). move/eqp_eq=> eq; exists (lead_coef p / lead_coef q). by rewrite mulf_neq0 // ?invr_eq0 lead_coef_eq0. by apply/(scaler_injl ulcq); rewrite scalerA mulrCA divrr // mulr1. by case=> c nz_c ->; apply/eqpP; exists (1, c); rewrite ?scale1r ?oner_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)