(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                                  misc.v                                  *)
(****************************************************************************)
Require Export Lci.

(****************)
Definition antisym (A : Set) (R : A -> A -> Prop) :=
  forall x y : A, R x y -> R y x -> x = y :>A.

(********************)
Definition pi1 : forall (A : Set) (P : A -> Prop), {x : A | P x} -> A.

Proof.
(* Goal: forall (A : Set) (P : forall _ : A, Prop) (_ : @sig A (fun x : A => P x)), A *)
simple induction 1; auto.
Defined.

(********************)
Lemma pi2 :
 forall (A : Set) (P : A -> Prop) (p : {x : A | P x}), P (pi1 A P p).

Proof.
(* Goal: forall (A : Set) (P : forall _ : A, Prop) (p : @sig A (fun x : A => P x)), P (pi1 A P p) *)
simple induction p; unfold pi1 in |- *; trivial.
Qed.

(*******************)
Definition inversible (S : Set) (Mult : S -> S -> S) 
  (I x : S) := exists y : S, Mult x y = I /\ Mult y x = I.

(************)
Lemma inv_com :
 forall (S : Set) (Mult : S -> S -> S) (I x : S),
 commutativity S Mult ->
 (exists y : S, Mult x y = I) -> inversible S Mult I x.

Proof.
(* Goal: forall (S : Set) (Mult : forall (_ : S) (_ : S), S) (I x : S) (_ : commutativity S Mult) (_ : @ex S (fun y : S => @eq S (Mult x y) I)), inversible S Mult I x *)
intros; unfold inversible in |- *.
(* Goal: @ex S (fun y : S => and (@eq S (Mult x y) I) (@eq S (Mult y x) I)) *)
elim H0; intros.
(* Goal: @ex S (fun y : S => and (@eq S (Mult x y) I) (@eq S (Mult y x) I)) *)
exists x0.
(* Goal: and (@eq S (Mult x x0) I) (@eq S (Mult x0 x) I) *)
split. 
(* Goal: @eq S (Mult x x0) I *)
(* Goal: @eq S (Mult x0 x) I *)
assumption.
(* Goal: @eq S (Mult x x0) I *)
(* Goal: @eq S (Mult x0 x) I *)
elim (H x x0); assumption.
Qed.  