proposition: Lemma unitrM_comm x y : comm x y -> (x * y \is a unit) = (x \is a unit) && (y \is a unit).
proof: Proof. move=> cxy; apply/idP/andP=> [Uxy | [Ux Uy]]; last by rewrite unitrMl. suffices Ux: x \in unit by rewrite unitrMr in Uxy. apply/unitrP; case/unitrP: Uxy => z [zxy xyz]; exists (y * z). rewrite mulrA xyz -{1}[y]mul1r -{1}zxy cxy -!mulrA (mulrA x) (mulrA _ z) xyz. by rewrite mul1r -cxy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)