Require MinMJ_booleans.
Require MinMJ_lt.

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

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

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

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

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).

Lemma nateqb_is_eq1 : (i,j:nat)i=j->(nateqb i j)=true.

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

Lemma nateqb_is_eq3 : (i,j:nat)(~i=j)->(nateqb i j)=false.

Lemma nateqb_is_eq4 : (i,j:nat)((nateqb i j)=false)->~i=j.

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).

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

Lemma nateq_dec : (i,j:nat)(nat_compare i j).

Lemma nateq_dec1 : (i,j:nat)(P:Prop)
		i=j->
		 ~i=j->
		  P.

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.

Lemma ltb_is_lt2 : (i,j:nat)
		(ltb i j)=true->(lt i j).

Lemma ltb_is_lt3 : (i,j:nat)
		~(lt i j)->(ltb i j)=false.

Lemma ltb_is_lt4 : (i,j:nat)
		(ltb i j)=false->~(lt i j).

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

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).

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

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

Lemma ltSplus2 : (i,j:nat)
		(lt i (S (plus j i))).

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

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

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

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

Lemma notltbii : (i,j:nat)
		i=j->
		 (ltb i j)=false.

Lemma ltplus2 : (j,h,i:nat)
		(lt i h)->
		 (lt i (plus j h)).

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

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

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

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

Lemma not_eq_notO_not_pred_eq : (i,j:nat)
	~i=O->
	 ~j=O->
	  ~i=j->
	   ~(pred i)=(pred j).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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).

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.

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

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))).

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))).

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

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

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