proposition: Lemma mpoly_intro_unit p q : q * p = 1 -> p \in mpoly_unit.
proof: Proof. move=> qp1; apply/andP; split; last first. apply/unitrP; exists q@_0. by rewrite 2!mulrC -rmorphM qp1 rmorph1. apply/eqP/msize1_polyC; have: msize (q * p) == 1%N. by rewrite qp1 msize1. have [-> | nz_p] := eqVneq p 0; first by rewrite mulr0 msize0. have [-> | nz_q] := eqVneq q 0; first by rewrite mul0r msize0. rewrite msizeM // (mpolySpred _ nz_p) (mpolySpred _ nz_q). by rewrite addnS addSn !eqSS addn_eq0 => /andP[] _ /eqP->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg