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.