Library group

Variable G : Set.
Variable operation : G -> G -> G.
Variable e : G.
Variable inv : G -> G.

Infix "×" := operation (at level 50, left associativity).

Hypothesis associativity : forall x y z : G, (x × y) × z = x × (y × z).
Hypothesis identity : forall x : G, (x × e) = e /\ e × x = x.
Hypothesis inverse : forall x : G, (x × inv x) = e /\ inv x × x = x.

Theorem latin_square_property : forall a b : G, exists x : G, a × x = b.
  intros a b.
  exists (inv a × b).
  rewrite <- associativity.
  destruct inverse with (x:=a) as [H _].
  rewrite H.
  destruct identity with (x:=b) as [_ H'].
  trivial.
Qed.