theory.groups

Require
  theory.setoids.
Require Import
  Morphisms abstract_algebra.

Section group_props.
Context `{Group G}.

Lemma inv_involutive x: - - x = x.

Global Instance: Injective (-).

Lemma inv_0: - mon_unit = mon_unit.

Global Instance: z : G, LeftCancellation (&) z.

Global Instance: z : G, RightCancellation (&) z.

Lemma sg_inv_distr `{!AbGroup G} x y: - (x & y) = - x & - y.
End group_props.

Section groupmor_props.
  Context `{Group A} `{Group B} {f : A B} `{!Monoid_Morphism f}.

  Lemma preserves_inv x: f (- x) = - f x.
End groupmor_props.

Instance semigroup_morphism_proper {A B eA eB opA opB} :
  Proper ((=) ==> iff) (@SemiGroup_Morphism A B eA eB opA opB) | 1.

Instance monoid_morphism_proper {A B eA eB opA uA opB uB} :
  Proper ((=) ==> iff) (@Monoid_Morphism A B eA eB opA uA opB uB) | 1.