proposition: Lemma modpD p q : (p + q) %% d = p %% d + q %% d.
proof: Proof. have/edivpP [] // : (p + q) = (p %/ d + q %/ d) * d + (p %% d + q %% d). by rewrite mulrDl addrACA -!divp_eq. apply: leq_ltn_trans (size_add _ _) _. rewrite gtn_max !ltn_modp andbb -lead_coef_eq0. by apply: contraTneq ulcd => ->; rewrite unitr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)