Section Group.

Variable A: Type.
Variable op: A -> A -> A.

Definition is_left_neutral  (e: A) := forall x: A, (op e x) = x.
Definition is_right_neutral (e: A) := forall x: A, x = (op x e).

Lemma uniqueness_of_neutral:
  forall a b: A, (is_left_neutral a) -> (is_right_neutral b) -> (a = b).
Proof.
  intro; intro.
  intros lna rnb.
  elim lna with b; elim rnb with a.
  reflexivity.
Qed.

End Group.

Definition is_left_neutral  (e: A) := forall x: A, x = (op e x).

Definition is_right_neutral (e: A) := forall x: A, (op x e) = x.