proposition: Lemma invrM : {in unit &, forall x y, (x * y)^-1 = y^-1 * x^-1}.
proof: Proof. move=> x y Ux Uy; have Uxy: (x * y \in unit) by rewrite unitrMl. by apply: (mulrI Uxy); rewrite divrr ?mulrA ?mulrK ?divrr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)