proposition: Lemma modpP p q r : p = q * d + r -> size r < size d -> r = (p %% d).
proof: Proof. by move/edivpP=> h; case/h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)