proposition: Lemma size_quot_eq0 : forall q d r : {poly R}, d \is monic -> size r < size d -> (size (q * d + r) < size d) = (q == 0).
proof: Proof. move=> q d r mon sz; apply/eqP/eqP => [sz0 | ->]; apply/eqP. - apply/negPn; apply/negP=> ab_absurdo; move: sz0. rewrite size_addl; last first. rewrite mulrC size_monicM //. have Htmp : 0 < size q by rewrite lt0n size_poly_eq0. rewrite -subn1 -addnBA //. apply leq_trans with (size d) => //. by rewrite leq_addr. rewrite mulrC size_monicM // prednK; last first. rewrite addn_gt0. apply/orP; left. by apply leq_ltn_trans with (size r). move/eqP. rewrite addnC -addnBA // subnn addn0 size_poly_eq0; by apply/negP. - by rewrite mul0r add0r subn_eq0. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly) ssralg_ext