Require MinMJ_booleans.
Require MinMJ_lt.

Lemma S1 : (i,j:nat)(i=j)->~i=(S j).
Intros.
Rewrite -> H.
(Generalize j ;Clear  H i j).
Induction j.
Discriminate.

Unfold not .
Intros.
Injection H0.
Auto.
Save.

Hint S1.

Lemma S2 : (i,j:nat)(i=j)->~i=(S (S j)).
Intros.
Rewrite -> H.
Clear  H i.
Elim j.
Discriminate.

Intros.
Injection.
Auto.
Save.

Hint S2.

Lemma Splus : (i,j:nat)(plus i (S j))=(S (plus i j)).
Induction i.
Auto.

Intros.
Simpl.
Rewrite -> (H j).
Auto.
Save.

Lemma Not_Splus : (i,j:nat)~(S (plus i j))=j.
Induction j.
Auto.

Unfold not .
Intros.
Apply H.
Rewrite <- (Splus i n).
Injection H0.
Auto.
Save.

Hint Not_Splus.

Recursive Definition nateqb : nat->nat->bool :=
O O => true |
(S i) O => false |
O (S j) => false |
(S i) (S j) => (nateqb i j).

Lemma nateqb_sym : (i,j:nat)(nateqb i j)=(nateqb j i).
Induction i.
Induction j.
Simpl.
Try Trivial.

Intros.
Simpl.
Try Trivial.

Induction j.
Simpl.
Try Trivial.

Intros.
Simpl.
Apply H.
Save.

Lemma nateqb_is_eq1 : (i,j:nat)i=j->(nateqb i j)=true.
Intros.
Rewrite -> H.
(Generalize j ;Clear  H j i).
Induction j.
Auto.

Intros.
Auto.
Save.

Lemma nateqb_is_eq2 : (i,j:nat)(nateqb i j)=true->i=j.
Induction i.
Induction j.
Auto.

Simpl.
Intros.
Discriminate H0.

Induction j.
Simpl.
(Intros d;Discriminate d).

Intros.
Simpl in H1.
Rewrite -> (H n0 H1).
Auto.
Save.

Lemma nateqb_is_eq3 : (i,j:nat)(~i=j)->(nateqb i j)=false.
Unfold not.
Intros.
Apply bool_dec5.
Unfold not.
Intros.
Apply H.
Apply (nateqb_is_eq2 i j H0).
Save.

Lemma nateqb_is_eq4 : (i,j:nat)((nateqb i j)=false)->~i=j.
Intros.
Cut (not (eq ? (nateqb i j) true)).
Unfold not.
Intros.
Apply H0.
Apply (nateqb_is_eq1 i j H1).

Apply bool_dec6.
Auto.
Save.

Definition nat_compare1 : nat->nat->Prop :=
[i,j:nat]((nateqb i j)=true)\/(nateqb i j)=false.

Lemma nateqb_dec : (i,j:nat)(nat_compare1 i j).
Unfold nat_compare1.
Intros.
Case (nateqb i j).
Left.
Try Trivial.

Right.
Try Trivial.
Save.

Definition nat_compare : nat->nat->Prop :=
[i,j:nat]i=j\/~i=j.

Lemma nateq_dec : (i,j:nat)(nat_compare i j).
Unfold nat_compare.
Intros.
Cut (nat_compare1 i j).
Unfold nat_compare1.
(Intros c;Elim c;[Clear  c;Intros c|Clear  c;Intros c]).
Left.
Apply (nateqb_is_eq2 i j c).

Right.
Apply nateqb_is_eq4.
Auto.

Exact (nateqb_dec i j).
Save.

Lemma nateq_dec1 : (i,j:nat)(P:Prop)
		i=j->
		 ~i=j->
		  P.
Intros.
Cut (eq ? (nateqb i j) true).
Rewrite -> (nateqb_is_eq3 i j H0).
(Intros d;Discriminate d).

Exact (nateqb_is_eq1 i j H).
Save.

Recursive Definition
    ltb : nat->nat->bool :=
	O O => false |
	O (S j) => true |
	(S i) O => false |
	(S i) (S j) => (ltb i j).

Lemma ltb_is_lt1 : (i,j:nat)
		(lt i j)->(ltb i j)=true.
Induction i.
Intros.
Inversion H.
Auto.

Intros.
Inversion H0.
Simpl.
Auto.
Save.

Lemma ltb_is_lt2 : (i,j:nat)
		(ltb i j)=true->(lt i j).
Induction i.
Induction j.
Simpl.
(Intros d;Discriminate d).

Auto.

Induction j.
Simpl.
(Intros d;Discriminate d).

Intros.
Apply lt_S.
Auto.
Save.

Lemma ltb_is_lt3 : (i,j:nat)
		~(lt i j)->(ltb i j)=false.
Unfold not.
Intros.
Apply bool_dec5.
Unfold not.
Intros.
Apply H.
Apply (ltb_is_lt2 i j H0).
Save.

Lemma ltb_is_lt4 : (i,j:nat)
		(ltb i j)=false->~(lt i j).
Intros.
Cut (not (eq ? (ltb i j) true)).
Unfold not.
Intros.
Apply H0.
Apply (ltb_is_lt1 i j H1).

Apply bool_dec6.
Auto.
Save.

Lemma lt_not_eq1 : (i,j:nat)
		(lt i j)->~i=j.
Induction i.
Induction j.
Intros.
Cut (eq ? (ltb O O) true).
Simpl.
(Intros d;Discriminate d).

Apply (ltb_is_lt1 O O H).

Auto.

Intros.
Inversion H0.
Unfold not  in H.
Injection.
Intros.
Apply (H j0 H2 H5).
Save.

Definition nat_compare2 : nat->nat->Prop :=
[i,j:nat](lt i j)\/i=j\/(lt j i).

Lemma natlt_dec : (i,j:nat)(nat_compare2 i j).
Intros.
Apply nat_double_ind.
Induction n.
Unfold nat_compare2.
Auto.

Unfold nat_compare2.
Intros.
Auto.

Unfold nat_compare2.
Auto.

Unfold nat_compare2.
Intros.
(Elim H;[Clear  H;Intros H|Clear  H;Intros H;Elim H;[Clear  H;Intros H|Clear  H;Intros H]]).
Left.
Apply lt_S.
Auto.

Auto.

(Right;Right).
(Apply lt_S;Auto).
Save.

Lemma ltS : (i,j:nat)
		(lt i j)->(lt i (S j)).
Induction i.
Auto.

Intros.
Apply lt_S.
Inversion H0.
Apply H.
Auto.
Save.

Hint ltS.
Hint nateq_dec.
Hint natlt_dec.

Lemma ltSplus1 : (i,j:nat)
		(lt i (S (plus i j))).
Induction i.
Auto.

Intros.
Simpl.
Apply lt_S.
Auto.
Save.

Hint ltSplus1.

Lemma ltSplus2 : (i,j:nat)
		(lt i (S (plus j i))).
Induction j.
Simpl.
Elim i.
Auto.

Intros.
Apply lt_S.
Auto.

Intros.
Simpl.
Apply ltS.
Auto.
Save.

Hint ltSplus2.

Lemma ltSplus3 : (i,j,k:nat)
		(lt i j)->
		 (lt i (S (plus k j))).
Induction k.
Simpl.
Intros.
Apply ltS.
Auto.

Intros.
Simpl.
Apply ltS.
Apply H.
Auto.
Save.

Hint ltSplus3.

Lemma ltplus1 : (i,j,k:nat)
		 (lt i k)->
		  (lt O j)->
		   (lt i (plus j k)).
Induction j.
Intros.
Inversion H0.

Induction k.
Intros.
Inversion H0.

Intros.
Simpl.
Apply ltSplus3.
Auto.
Save.

Hint ltplus1.

Lemma plus_bridge : (i,j:nat)
		(plus i (S j))=(S (plus i j)).
Induction i.
Auto.

Intros.
Simpl.
Rewrite -> H.
Auto.
Save.

Lemma Slt : (i,j:nat)
		(lt (S i) j)->
		 (lt i j).
Induction j.
Intros.
Inversion H.

Intros.
Inversion H0.
Apply ltS.
Auto.
Save.

Lemma notltbii : (i,j:nat)
		i=j->
		 (ltb i j)=false.
Intros.
Rewrite -> H.
(Generalize j ;Clear  H j i).
Induction j.
Auto.

Intros.
Auto.
Save.

Lemma ltplus2 : (j,h,i:nat)
		(lt i h)->
		 (lt i (plus j h)).
Induction h.
Intros.
Inversion H.

Intros.
Inversion H0.
Rewrite -> plus_bridge.
Auto.

Rewrite -> plus_bridge.
Apply lt_S.
Apply (H i0).
Auto.
Save.

Hint ltplus2.

Lemma lt_trans : (k,i,j:nat)
		(lt i j)->
		 (lt j k)->
		  (lt i k).
Induction k.
(Intros;Inversion H0).

Induction i.
Auto.

Induction j.
(Intros d;Inversion d).

Intros.
(Inversion_clear H2;Inversion_clear H3).
Apply lt_S.
Apply H with j:=n1 .
Auto.

Auto.
Save.

Lemma lt_trans1 : (i,k,j:nat)
		(lt i j)->
		 (lt j k)->
		  (lt (S i) k).
Induction i.
Intros k j H.
Inversion_clear H.
Intros.
Inversion_clear H.
Inversion_clear H0.
Apply lt_S.
Apply lt_O.

Apply lt_S.
Apply lt_O.

Intros.
(Generalize H1 ; Clear  H1; Inversion_clear H0).
Intros.
Inversion_clear H0.
Apply lt_S.
Apply (H j1 j0).
Auto.

Auto.
Save.

Lemma ltnotlt : (i,j:nat)
	(lt i j)->~(lt j i).
Intros.
Apply ltb_is_lt4.
(Generalize i j H ;Clear  H i j).
Induction i.
Intros.
Simpl.
Apply ltb_is_lt3.
Unfold not .
Intros.
Inversion H0.

Intros.
Inversion_clear H0.
Simpl.
Apply H.
Auto.
Save.

Hint ltnotlt.

Lemma ltnot0 : (i,j:nat)
	(lt i j)->~j=O.
Intros.
Inversion_clear H.
Discriminate.

Discriminate.
Save.

Lemma not_eq_notO_not_pred_eq : (i,j:nat)
	~i=O->
	 ~j=O->
	  ~i=j->
	   ~(pred i)=(pred j).
Induction i.
Unfold not .
Intros.
Apply H.
Auto.

Induction j.
Unfold not .
Intros.
Apply H1.
Auto.

Intros.
Simpl.
Unfold not  in H3.
Unfold not .
Intros.
Apply H3.
Auto.
Save.

Lemma ltiSi : (i,j:nat)
	i=j->
	 (lt i (S j)).
Intros.
Apply ltb_is_lt2.
Rewrite -> H.
Elim j.
Auto.

Intros.
Auto.
Save.

Hint ltiSi.

Lemma notltii : (i,j:nat)
	i=j->
	 ~(lt i j).
Induction i.
Intros.
Rewrite <- H.
Apply ltb_is_lt4.
Auto.

Intros.
Rewrite <- H0.
Apply ltb_is_lt4.
Simpl.
Apply ltb_is_lt3.
Apply H.
Auto.
Save.

Hint notltii.

Lemma ltS_ltpred : (i,j:nat)
	 (lt (S i) j)->
	  (lt i (pred j)).
Induction j.
Intros.
Inversion H.

Intros.
Simpl.
Inversion_clear H0.
Auto.
Save.

Hint ltS_ltpred.

Lemma ltpred_ltS : (i,j:nat)
	(lt i (pred j))->
	 (lt (S i) j).

Induction j.
Intros.
Inversion H.

Intros.
Simpl in H0.
Auto.
Save.

Lemma lt_S_le : (j,i:nat)
	(lt i j)->
	 (S i)=j\/(lt (S i) j).

Induction j.
Intros.
Inversion H.

Intros.
Cut (nat_compare2 i n).
Unfold nat_compare2 .
(Intros d; Case d; Clear  d; Intros d).
Right.
Apply lt_S.
Auto.

(Case d; Clear  d; Intros d).
Left.
Auto.

(Generalize d ; Clear  d).
Inversion_clear H0.
Intros.
Inversion d.

Intros.
Cut (or (eq ? (S i0) n) (lt (S i0) n)).
Intros.
Case H0.
Clear  H0.
Intros.
Rewrite -> H0.
Left.
Auto.

Clear  H0.
Intros.
Right.
Apply lt_S.
Auto.

Apply H.
Auto.
Exact (natlt_dec i n).
Save.

Hint lt_S_le.

Lemma lt_S_le2 : (i,j:nat)
	(lt i (S j))->
	 (lt i j)\/i=j.

(Intros; Cut (or (eq ? (S i) (S j)) (lt (S i) (S j)))).
(Intros c; Case c; Clear  c; Intros).
(Injection H0; Auto).

(Inversion_clear H0; Auto).

(Apply lt_S_le; Auto).
Save.

Hint lt_S_le2.

Lemma lt_trans2 : (i,j,k:nat) 
	(lt i (S j))->
	 (lt j k)->
	  (lt i k).

Induction i.
Intros.
Inversion H0.
Auto.

Auto.

Intros.
Apply lt_trans1 with j:=j.
Inversion_clear H0.
Auto.

Auto.
Save.

Lemma lt_trans3 : (i,j,k:nat)
	(lt i j)->
	 (lt j (S k))->
	  (lt i k).

(Induction j; Clear  j; Intros).
Inversion H.

Inversion_clear H1.
(Apply lt_trans2 with j:=n; Auto).
Save.

Lemma not_lt_eq_lt : (i,j:nat)
	~(lt i j)->
	 i=j\/(lt j i).

Intros.
Cut (nat_compare2 i j).
Unfold nat_compare2 .
Intros.
(Case H0; Clear  H0; Intros).
Left.
Apply nateqb_is_eq2.
Apply bool_dec4.
(Unfold not  in H; Unfold not ; Intros).
Apply H.
Auto.

Auto.

Exact (natlt_dec i j).
Save.

Hint not_lt_eq_lt.

Lemma ltS_neq_lt : (j,i:nat)
	(lt i (S j))->
	 ~i=j->
	  (lt i j).

Induction j.
Intros.
Generalize H0 .
Clear  H0.
Inversion_clear H.
Intros.
Apply nateq_dec1 with i:=O j:=O.
Auto.

Auto.

Inversion_clear H0.

Intros.
(Generalize H1 ; Clear  H1; Inversion_clear H0).
Auto.

Intros.
Apply lt_S.
Apply H.
Auto.

(Unfold not  in H0; Unfold not ; Intros).
Auto.
Save.

Lemma lt_not_ltpred : (i,j:nat)
	(lt i j)->
	 ~(lt (pred j) i).

Induction j.
Intros.
Inversion H.

Intros.
Simpl.
Cut (or (eq ? (S i) (S n)) (lt (S i) (S n))).
(Intros c; Case c; Clear  c; Intros).
(Injection H1; Intros).
Apply notltii.
Auto.

Inversion_clear H1.
Apply ltnotlt.
Auto.

Apply lt_S_le.
Auto.
Save.

Lemma lt_not_ltS : (i,j:nat)
	(lt i j)->
	 ~(lt j (S i)).

(Intros; Cut (eq ? j (pred (S j))); Auto; Intros; Rewrite -> H0;
 Apply lt_not_ltpred; Auto).
Save.

Lemma plus_eq2 : (i,j:nat)
	(plus (S i) j)=
	 (S (plus i j)).

Auto.
Save.

Lemma plus_right_id : (i:nat)
	(plus i O)=i.

(Induction i; Clear  i; Auto).
Save.

Lemma sym_plus : (i,j:nat)
	(plus i j)=(plus j i).

(Induction i; Clear  i; Intros; Simpl).
(Rewrite -> plus_right_id; Auto).

(Rewrite -> H; Auto).
Save.

Lemma ltS_not_lt : (i,j:nat)
	(lt i (S j))->
	 ~(lt j i).

Intros.
Cut (or (eq ? (S i) (S j)) (lt (S i) (S j))).
(Intros c; Case c; Clear  c; Intros).
(Injection H0; Intros; Apply notltii; Auto).

(Apply ltnotlt; Inversion H0; Auto).

(Apply lt_S_le; Auto).
Save.

Lemma ltplus3 : (i,j:nat)
	(lt O j)->
	 (lt i (plus j i)).

Induction j.
(Intros H; Inversion H).

Intros.
Simpl.
Apply ltSplus2.
Save.

Lemma ltplus4 : (i,j,k:nat)
	(lt (plus i j) k)->
	 (lt i k).

(Induction i; Clear  i; Simpl; Intros).
(Inversion_clear H; Auto).

Inversion_clear H0.
Apply lt_S.
(Apply (H j); Auto).
Save.

Lemma ltplus6: (i,j,k,n:nat)
	(lt k i)->
	 (lt n j)->
	  (lt (plus k n) (plus i j)).

(Induction i; Clear  i; Simpl).
Intros.
Inversion H.

Intros.
Cut (or (eq ? (S k) (S n)) (lt (S k) (S n))).
(Intros c; Case c; Clear  c H0; Intros).
(Injection H0; Clear  H0; Intros).
Rewrite -> H0.
(Elim n; Simpl; Intros).
(Apply ltS; Auto).

Auto.

(Inversion_clear H0; Apply ltS; Apply H; Auto).

(Apply lt_S_le; Auto).
Save.

Lemma ltplus5: (k,j,i,n:nat)
	(lt (plus i j) (plus k n))->
	 (lt i k)\/(lt j k)\/(lt i n)\/(lt j n).

Intros.
(Cut (nat_compare2 i k); Auto; Unfold nat_compare2 ; Intros c; 
 Case c; Clear  c; Intros c; Auto; Case c; Clear  c; Intros).
(Generalize H ; Rewrite -> H0; Clear  H H0 i; Intros).
(Right; Right; Right).
(Generalize H ; Clear  H; Elim k; Simpl; Auto; Intros).
(Inversion_clear H0; Apply H; Auto).

(Cut (nat_compare2 j n); Auto; Unfold nat_compare2 ; Intros c; 
 Case c; Clear  c; Intros c; Auto; Case c; Clear  c; Intros).
(Generalize H ; Rewrite -> H1; Clear  H H1 j; Intros).
Left.
(Generalize H ; Clear  H; Elim n).
(Rewrite -> plus_right_id; Rewrite -> plus_right_id; Auto).

Intros n0 H.
(Rewrite -> sym_plus; Rewrite -> plus_eq2; Rewrite -> (sym_plus k);
 Rewrite -> plus_eq2; Rewrite -> sym_plus; Rewrite -> (sym_plus n0);
 Intros).
(Inversion_clear H1; Apply H; Auto).

Cut False.
Contradiction.

Cut (not (lt (plus i j) (plus k n))).
(Intros H2; Apply H2; Auto).

Apply ltnotlt; Apply ltplus6; Auto.
Save.

Recursive Definition 
    max_nat : nat->nat->nat :=
	i j => (Setifb nat (ltb i j) j i).

Lemma max_nat0 : (i:nat)
	(max_nat i O)=i.

(Induction i; Clear  i; Simpl; Auto).
Save.

Lemma sym_max_nat : (i,j:nat)
	(max_nat i j)=(max_nat j i).

(Intros; Cut (nat_compare2 i j); Auto; Unfold nat_compare2; Intros c;
 Case c; Clear  c; Intros; Unfold max_nat).
(Rewrite -> ltb_is_lt1; Auto; Rewrite -> ltb_is_lt3; Auto).

(Case H; Clear  H; Intros).
Repeat (Rewrite -> ltb_is_lt3; Auto).

(Rewrite -> ltb_is_lt3; Auto; Rewrite -> ltb_is_lt1; Auto).
Save.

Lemma lt_max_nat : (i,j,k:nat)
	(lt i (S (max_nat j k)))->
	 ((lt i (S j)) /\ (lt k (S j)))\/
	  ((lt i (S k)) /\ (lt j (S k))).

(Unfold max_nat; Intros; Generalize H ; Clear  H;
 Cut (nat_compare2 j k); Auto; Unfold nat_compare2; Intros c; Case c;
 Clear  c; Intros c).
(Rewrite -> ltb_is_lt1; Auto; Simpl; Intros; Right; Split; Auto).

(Case c; Clear  c; Intros c; Rewrite -> ltb_is_lt3; Auto).
Save.

Lemma eq_max_nat : (i,j,k:nat)
	i=(S (max_nat j k))->
	 (i=(S j)/\ (lt k (S j)))\/
	  (i=(S k)/\ (lt j (S k))).

(Unfold max_nat; Intros; Generalize H ; Clear  H;
 Cut (nat_compare2 j k); Auto; Unfold nat_compare2; Intros c; Case c;
 Clear  c; Intros c).
(Rewrite -> ltb_is_lt1; Auto; Simpl; Intros; Right; Split; Auto).

(Case c; Clear  c; Intros c; Rewrite -> ltb_is_lt3; Auto).
Save.

Lemma lt_max_nat1 : (i,j,k:nat)
	i=j->
	 (lt i (S (max_nat j k))).

(Unfold max_nat; Intros; Generalize H ; Clear  H;
 Cut (nat_compare2 j k); Auto; Unfold nat_compare2; Intros c; Case c;
 Clear  c; Intros c).
(Rewrite -> ltb_is_lt1; Auto).
(Simpl; Intros; Rewrite -> H; Auto).

(Case c; Clear  c; Intros; Rewrite -> ltb_is_lt3; Auto).
Save.

Lemma lt_max_nat2 :
	(i,j,k:nat)
	 (lt i j)->
	  (lt i (max_nat j k)).

(Intros; Cut (nat_compare2 j k); Auto; Unfold nat_compare2 ; Intros c;
 Case c; Clear  c; Intros; Unfold max_nat ).
(Rewrite -> ltb_is_lt1; Auto; Apply lt_trans with j:=j; Auto).

(Case H0; Clear  H0; Intros; Rewrite -> ltb_is_lt3; Auto).
Save.

Lemma S_max_nat_bridge0 :
	(i,j:nat)
	 (S (max_nat i j))=(max_nat (S i) (S j)).

(Intros; Unfold max_nat; Cut (nat_compare2 i j); Auto;
 Unfold nat_compare2; Intros c; Case c; Clear  c; Intros).
Repeat (Rewrite -> ltb_is_lt1; Auto).

(Case H; Clear  H; Intros; Repeat (Rewrite -> ltb_is_lt3; Auto)).
Save.

Hint lt_max_nat.
Hint lt_max_nat1.
Hint lt_max_nat2.