Groups

foo.v

Variable G : Set.
Variable e : G.

Variable inv : G -> G.
Variable mult : G -> G -> G.
Infix "*" := mult.

Axiom left_id : forall x : G, e * x = x.
Axiom left_inv : forall x : G, inv x * x = e.
Axiom assoc : forall x y z : G, x * (y * z) = (x * y) * z.

Theorem right_id : forall x : G, x * e = x.
Proof.
  intros x.
  assert (inv x * (x * e) = inv x * x) as H.
    rewrite assoc.
    rewrite left_inv.
    apply left_id.
  apply left_cancel in H.
  exact H.
Qed.