Some algebra proof about Group using Coq.

groups.v

Section Group.

Variable G : Set.
Variable op : G -> G -> G.
Infix "o" := op (at level 35, right associativity).
Axiom assoc : forall a b c : G, a o (b o c) = (a o b) o c.
Variable e : G.
Axiom unit_l : forall a : G, e o a = a.
Axiom unit_r : forall a : G, a o e = a.
Axiom inv_l : forall a : G, exists b : G, b o a = e.
Axiom inv_r : forall a : G, exists b : G, a o b = e.

Goal forall a b c : G, a o b = a o c -> b = c.
Proof.
intros.
rewrite <- unit_l with b.
rewrite <- unit_l with c.
elim (inv_l a).
intros.
rewrite <- H0.
rewrite <- assoc.
rewrite <- assoc.
rewrite <- H.
reflexivity.
Qed.

Goal forall a b c : G, (a o b = e) /\ (b o a = e) /\ (a o c = e) /\ (c o a = e) -> b = c.
Proof.
intros.
rewrite <- unit_l with b.
decompose [and] H.
rewrite <- H4.
rewrite <- assoc.
rewrite H0.
rewrite unit_r.
reflexivity.
Qed.

End Group.