proposition: Lemma rdivp_l_eq p : p = d * (rdivp_l p d) + (rmodp_l p d).
proof: Proof. have mon_phi_d: phi d \is monic by rewrite monic_map_inj. apply: (can_inj (@phiK R)); rewrite {1}[phi p](rdivp_eq mon_phi_d) rmorphD. rewrite rmorphM /rdivp_l /rmodp_l /redivp_l /rdivp /rmodp. by case: (redivp _ _)=> [[k q'] r'] /=; rewrite !phi_invK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype fintype finfun ssrnat seq) mathcomp(choice ssralg poly polydiv mxpoly matrix bigop) mathcomp(mxalgebra perm fingroup tuple) mxstructure dvdring