proposition: Lemma eqp_rmod_mod p q : rmodp p q %= modp p q.
proof: Proof. rewrite modpE 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)