proposition: Lemma gauge_inv A : gauge A -> gauge (A^-1)%classic.
proof: Proof. case=> n _ EA; apply: (@filterS _ _ _ (iter n split_sym (E `&` E^-1))). - exact: gauge_filter. - by case: n EA; last move=> n; move=> EA [? ?] [/=] ? ?; exact: EA. - by exists n . Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed