Section lexicografica.
Open Scope type_scope.

Variables A B:Set.
Definition P:=fun _:A => B.
Check P.

Print sigS.

Lemma e1:(sigS P) -> A*B.
intro H. 
case H;intros a b.
clear H.

Print prod.

exact (a,b).
Defined.

Lemma e2:A*B->(sigS P).
intro H.
case  H;intros.
exact (existS P a b).
Defined.

Print e2.

Definition ee2 (x:A*B):=
let a := (fst x) in
let b:= (snd x) in
(existS P a b).

Lemma e2r:forall x:A*B, e2 x=existS P (fst x) (snd x).
destruct x.
auto.
Qed.

Theorem uno:forall (a:A) (b:B),e1 (e2 (a,b)) = (a,b).
simpl;
auto.
Qed.

Theorem dos:forall (a:A) (b:B),
e2 (e1 (existS P a b)) = existS P a b.
simpl;auto.
Qed.

Variable leA:A->A->Prop.
Variable leB:B->B->Prop.

Variable wfA:well_founded leA.
Variable wfB:well_founded leB.



Require Export Wellfounded.

Require Export Relations.


Definition lexic_A_B (x y : (A*B)) : Prop :=
 (leA (fst x) (fst y))
  \/ (fst x) =(fst y) /\ (leB (snd x) (snd y)) .

Check lexprod.
Print lexprod.

Lemma implic1:forall x y:A*B, lexic_A_B x y ->
(lexprod A P leA (fun _:A=>leB) (e2 x) (e2 y)).
Proof.
intros x y H .
repeat rewrite e2r.

case H;intros H0.
Show 2.
constructor;auto.

case H0;intros ig men.
rewrite ig.
constructor 2;auto.
Qed.

Lemma inverselexic:well_founded
           (fun x y : A * B =>
            lexprod A P leA (fun _ : A => leB) (e2 x) (e2 y)).
apply (wf_inverse_image (A*B) (sigS P) 
(lexprod A P leA (fun _:A=>leB)) e2  ).
apply wf_lexprod;[exact wfA|intros;exact wfB].
Qed.

Definition R' (x y:A*B):Prop:=
   lexprod A P leA (fun _ : A => leB) (e2 x) (e2 y).

Lemma subrel:forall (A:Set)(R R':A->A->Prop),
(inclusion A R R')->(well_founded R')->
(well_founded R).
Proof.
intros A0 R0 R1 Inc.
unfold well_founded.
intros.
unfold inclusion in Inc.
elim (H a).
intros.
split;intros.
apply (H1 y).
apply Inc;auto.
Qed.

Theorem wfR:well_founded lexic_A_B.
apply subrel with R'.
unfold inclusion.
unfold R'.
intros.
apply implic1;auto.
apply inverselexic.
Qed.

End lexicografica.


Check lexic_A_B.
Check wfR.