proposition: Lemma invmxZ a A : a *: A \in unitmx -> invmx (a *: A) = a^-1 *: invmx A.
proof: Proof. rewrite /invmx !unitmxE detZ unitrM => /andP[Ua U_A]. rewrite Ua U_A adjZ !scalerA invrM {U_A}//=. case: (posnP n) A => [-> | n_gt0] A; first by rewrite flatmx0 [_ *: _]flatmx0. rewrite unitrX_pos // in Ua; rewrite -[_ * _](mulrK Ua) mulrC -!mulrA. by rewrite -exprSr prednK // !mulrA divrK ?unitrX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)