proposition: Lemma leq_rmodp m d : size (rmodp m d) <= size m.
proof: Proof. have [/rmodp_small -> //|h] := ltnP (size m) (size d). have [->|d0] := eqVneq d 0; first by rewrite rmodp0. by apply: leq_trans h; apply: ltnW; rewrite ltn_rmodp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)