proposition: Lemma monic_lreg (p : {poly R}) : p \is monic -> GRing.lreg p.
proof: Proof. by rewrite monicE=> /eqP h; apply/lreg_lead; rewrite h; apply/lreg1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice matrix bigop zmodp poly polydiv mxpoly) CoqEAL(minor hrel param refinements seqmx)