# 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.

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.

This page has been generated by coqdoc