X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fcompare.ma;h=c701cd2e7175c635e1ec67d93b9f0afed1ed8526;hb=562e9adf40098e11d8f0bc2711a7f665360c2231;hp=2647315804661a23db188e36b4955c0b01c5152a;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/library/nat/compare.ma b/matita/library/nat/compare.ma
index 264731580..c701cd2e7 100644
--- a/matita/library/nat/compare.ma
+++ b/matita/library/nat/compare.ma
@@ -112,23 +112,60 @@ match n with
 	match m with 
         [ O \Rightarrow false
 	| (S q) \Rightarrow leb p q]].
-	
+
+theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
+(n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
+P (leb n m).
+apply nat_elim2; intros; simplify
+  [apply H.apply le_O_n
+  |apply H1.apply not_le_Sn_O.
+  |apply H;intros
+    [apply H1.apply le_S_S.assumption.
+    |apply H2.unfold Not.intros.apply H3.apply le_S_S_to_le.assumption
+    ]
+  ]
+qed.
+
+(*
+theorem decidable_le: \forall n,m. n \leq m \lor n \nleq m. 
+intros.
+apply (leb_elim n m)
+  [intro.left.assumption
+  |intro.right.assumption
+  ]
+qed.
+*)
+
+theorem le_to_leb_true: \forall n,m. n \leq m \to leb n m = true.
+intros.apply leb_elim;intros
+  [reflexivity
+  |apply False_ind.apply H1.apply H.
+  ]
+qed.
+
+theorem lt_to_leb_false: \forall n,m. m < n \to leb n m = false.
+intros.apply leb_elim;intros
+  [apply False_ind.apply (le_to_not_lt ? ? H1). assumption
+  |reflexivity
+  ]
+qed.
+
 theorem leb_to_Prop: \forall n,m:nat. 
 match (leb n m) with
 [ true  \Rightarrow n \leq m 
 | false \Rightarrow n \nleq m].
-intros.
-apply (nat_elim2
-(\lambda n,m:nat.match (leb n m) with
-[ true  \Rightarrow n \leq m 
-| false \Rightarrow n \nleq m])).
-simplify.exact le_O_n.
-simplify.exact not_le_Sn_O.
-intros 2.simplify.elim ((leb n1 m1)).
-simplify.apply le_S_S.apply H.
-simplify.unfold Not.intros.apply H.apply le_S_S_to_le.assumption.
+apply nat_elim2;simplify
+  [exact le_O_n
+  |exact not_le_Sn_O
+  |intros 2.simplify.
+   elim ((leb n m));simplify
+    [apply le_S_S.apply H
+    |unfold Not.intros.apply H.apply le_S_S_to_le.assumption
+    ]
+  ]
 qed.
 
+(*
 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
 (n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
 P (leb n m).
@@ -142,6 +179,7 @@ elim (leb n m).
 apply ((H H2)).
 apply ((H1 H2)).
 qed.
+*)
 
 let rec nat_compare n m: compare \def
 match n with