proposition: Lemma ltn_rmodp p q : (size (rmodp p q) < size q) = (q != 0).
proof: Proof. rewrite /rdivp /rmodp /rscalp unlock; have [->|q0] := eqVneq q 0. by rewrite /= size_poly0 ltn0. elim: (size p) 0%N 0 {1 3}p (leqnn (size p)) => [|n ihn] k q1 r. move/size_poly_leq0P->. by rewrite /= size_poly0 size_poly_gt0 q0 size_poly0 size_poly_gt0. move=> hr /=; case: (ltnP (size r)) => // hsrq; apply/ihn/leq_sizeP => j hnj. rewrite coefB -scalerAl !coefZ coefXnM coefMC ltn_subRL ltnNge. have sq: 0 < size q by rewrite size_poly_gt0. have sr: 0 < size r by apply: leq_trans hsrq. have hj: (size r).-1 <= j by apply: leq_trans hnj; rewrite -ltnS prednK. move: (leq_add sq hj); rewrite add1n prednK // => -> /=. move: hj; rewrite leq_eqVlt prednK // => /predU1P [<- | hj]. by rewrite -predn_sub subKn // !lead_coefE subrr. have/leq_sizeP -> //: size q <= j - (size r - size q). by rewrite subnBA // leq_subRL ?leq_add2r // (leq_trans hj) // leq_addr. by move/leq_sizeP: hj => -> //; rewrite mul0r mulr0 subr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)