proposition: Lemma commrV x y : comm x y -> comm x y^-1.
proof: Proof. have [Uy cxy | /invr_out-> //] := boolP (y \in unit). by apply: (canLR (mulrK Uy)); rewrite -mulrA cxy mulKr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)