# cantor.v

1 Variable G : Set.
2 Variable operation : G -> G -> G.
3 Variable e : G.
4 Variable inv : G -> G.
5
6 Infix × := operation (at level 50, left associativity).
7
8 Hypothesis associativity : forall x y z : G, (x × y) × z = x × (y × z).
9 Hypothesis identity : forall x : G, (x × e) = e /\ e × x = x.
10 Hypothesis inverse : forall x : G, (x × inv x) = e /\ inv x × x = x.
11
12 Theorem latin_square_property : forall a b : G, exists x : G, a × x = b.
13 intros a b.
14 exists (inv a × b).
15 rewrite <- associativity.
16 destruct inverse with (x:=a) as [H _].
17 rewrite H.
18 destruct identity with (x:=b) as [_ H'].
19 trivial.
20 Qed.