proposition: Lemma ltn_rmodp_l p q : (size (rmodp_l p q) < size q) = (q != 0).
proof: Proof. have := ltn_rmodp (phi p) (phi q). rewrite -(rmorph0 phi) (inj_eq (can_inj phiK)) => <-. rewrite /rmodp_l /redivp_l /rmodp; case: (redivp _ _)=> [[k q'] r'] /=. by rewrite !size_map_inj_poly. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype finfun perm matrix bigop zmodp mxalgebra) mathcomp(choice poly polydiv mxpoly binomial)