proposition: Lemma rmodpXnSm (p : {poly A}) a n m : rmodp (p * 'X^n + a%:P) 'X^m.+1 = if (n <= m.+1)%C then (rmodp p 'X^(m.+1 - n)) * 'X^n + a%:P else a%:P.
proof: Proof. have [leqnSm|gtnSm] := leqP n m.+1. rewrite [(_ <= _)%C]leqnSm. rewrite [p in LHS](@rdivp_eq _ 'X^(m.+1 - n)) ?monicXn //. rewrite mulrDl -addrA -mulrA -exprD subnK ?rmodp_addl_mul_small //. by rewrite monicXn. rewrite size_polyXn (leq_ltn_trans (size_add _ _)) // gtn_max. rewrite (leq_ltn_trans (size_mul_leq _ _)) /=. by rewrite size_polyC; case: (a != 0). rewrite size_polyXn addnS -pred_Sn addnC -ltn_subRL [X in (_ < X)]subSn //. by rewrite -[X in (_ < X)](size_polyXn A) ltn_rmodp monic_neq0 ?monicXn. rewrite ifN -?ltnNge // -[in LHS](subnK (ltnW gtnSm)) exprD mulrA. by rewrite rmodp_addl_mul_small ?monicXn ?size_polyC ?size_polyXn; case: (a != 0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg bigop poly polydiv) CoqEAL(param refinements pos hrel poly_op)