proposition: Lemma invrK : involutive (@inv R).
proof: Proof. move=> x; case Ux: (x \in unit); last by rewrite !invr_out ?Ux. rewrite -(mulrK Ux _^-1) -mulrA commrV ?mulKr //. by apply/unitrP; exists x; rewrite divrr ?mulVr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)