Require MinMJ_Exchange.

Lemma V_Exchange_inv :
	(x:V)(i,j:nat)
	 i=j->
	  (V_Exchange i (V_Exchange j x))=x.

(Intros; Rewrite -> H; Clear  H i;
 Cut (nat_compare j x); [ Destruct 1; Intro | Auto ];
 Unfold 2 V_Exchange).
(Rewrite -> nateqb_is_eq1; Auto; Simpl; Unfold V_Exchange).
(Rewrite -> nateqb_is_eq3; Auto; Rewrite -> nateqb_is_eq1; Auto).

(Rewrite -> nateqb_is_eq3; Auto;
 Cut (nat_compare (S j) x); [ Destruct 1; Intro | Auto ]).
(Rewrite -> nateqb_is_eq1; Auto; Simpl; Unfold V_Exchange).
(Rewrite -> nateqb_is_eq1; Auto).

(Rewrite -> nateqb_is_eq3; Auto; Simpl; Unfold V_Exchange).
(Rewrite -> nateqb_is_eq3; Auto; Rewrite -> nateqb_is_eq3; Auto).
Save.

Lemma L_Exchange_inv :
	(l:L)(i,j:nat)
	 i=j->
	  (L_Exchange i (L_Exchange j l))=l.

(Induction l; Clear  l; Intros; Auto).
(Rewrite -> L_Exchange_eq1; Rewrite -> L_Exchange_eq1;
 Rewrite -> V_Exchange_inv; Auto).

(Simpl; Rewrite -> V_Exchange_inv; Auto; Rewrite -> H; Auto;
 Rewrite -> H0; Auto).

(Simpl; Rewrite -> H; Auto).
Save.