右単位元とそれに関する右逆元だけで群を定義できることの証明

Group.v

Require Import Coq.Setoids.Setoid.

Record Group:Type := {
  g_set : Type;
  g_mult : g_set -> g_set -> g_set;
  g_assoc a b c : g_mult (g_mult a b) c = g_mult a (g_mult b c);
  g_id : g_set;
  g_id_r a : g_mult a g_id = a;
  g_inv : g_set -> g_set;
  g_inv_r a : g_mult a (g_inv a) = g_id
}.

Notation "x * y" := (g_mult _ x y).
Notation "1" := (g_id _).
Notation "/ x" := (g_inv _ x).

Theorem g_inv_l G (a:g_set G) : /a * a = 1.
Proof.
  rewrite <-(g_id_r _ (/a*a)).
  rewrite <-(g_inv_r _ (/a)) at 1.
  rewrite <-g_assoc.
  rewrite (g_assoc _ (/a) a).
  rewrite g_inv_r.
  rewrite g_id_r.
  apply g_inv_r.
Qed.

Theorem g_id_l G (a:g_set G) : 1 * a = a.
Proof.
  rewrite <-(g_inv_r _ a).
  rewrite g_assoc.
  rewrite g_inv_l.
  apply g_id_r.
Qed.