proposition: Lemma modp_id p q : (p %% q) %% q = p %% q.
proof: Proof. by have [->|qn0] := eqVneq q 0; rewrite ?modp0 // modp_small ?ltn_modp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)