proposition: Lemma eqp_rdiv_div p q : rdivp p q %= divp p q.
proof: Proof. rewrite divpE eqp_sym; case: ifP=> ulcq //; apply: eqp_scale; rewrite invr_eq0 //. by apply: expf_neq0; apply: contraTneq ulcq => ->; rewrite unitr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)