Require Export Lci.

Definition antisym (A : Set) (R : A → A → Prop) :=
  ∀ x y : A, R x y → R y x → x = y :>A.

Definition pi1 : ∀ (A : Set) (P : A → Prop), {x : A | P x} → A.
Proof.
simple induction 1; auto.
Defined.

Lemma pi2 :
 ∀ (A : Set) (P : A → Prop) (p : {x : A | P x}), P (pi1 A P p).
Proof.
simple induction p; unfold pi1 in |- *; trivial.
Qed.

Definition inversible (S : Set) (Mult : S → S → S)
  (I x : S) := ∃ y : S, Mult x y = I ∧ Mult y x = I.

Lemma inv_com :
 ∀ (S : Set) (Mult : S → S → S) (I x : S),
 commutativity S Mult →
 (∃ y : S, Mult x y = I) → inversible S Mult I x.
Proof.
intros; unfold inversible in |- ×.
elim H0; intros.
∃ x0.
split.
assumption.
elim (H x x0); assumption.
Qed.