- { is_monoid:> isMonoid G;
- inv_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (inv G);
- inv_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (inv G)
+ { is_monoid :> IsMonoid G;
+ inv_is_left_inverse : is_left_inverse G (inv G);
+ inv_is_right_inverse: is_right_inverse G (inv G)