X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fcompare.ma;h=b002d78cccdedd6ad690ffeea67aaa0402c14288;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=c701cd2e7175c635e1ec67d93b9f0afed1ed8526;hpb=f275a4daa42f8ab455020ec5a7ce7bf69b460c37;p=helm.git

diff --git a/helm/software/matita/library/nat/compare.ma b/helm/software/matita/library/nat/compare.ma
index c701cd2e7..b002d78cc 100644
--- a/helm/software/matita/library/nat/compare.ma
+++ b/helm/software/matita/library/nat/compare.ma
@@ -126,6 +126,23 @@ apply nat_elim2; intros; simplify
   ]
 qed.
 
+theorem leb_true_to_le:\forall n,m.
+leb n m = true \to (n \le m).
+intros 2.
+apply leb_elim
+  [intros.assumption
+  |intros.destruct H1.
+  ]
+qed.
+
+theorem leb_false_to_not_le:\forall n,m.
+leb n m = false \to \lnot (n \le m).
+intros 2.
+apply leb_elim
+  [intros.destruct H1
+  |intros.assumption
+  ]
+qed.
 (*
 theorem decidable_le: \forall n,m. n \leq m \lor n \nleq m. 
 intros.
@@ -181,6 +198,50 @@ apply ((H1 H2)).
 qed.
 *)
 
+definition ltb ≝λn,m. leb n m ∧ notb (eqb n m).
+
+theorem ltb_to_Prop :
+ ∀n,m.
+  match ltb n m with
+  [ true ⇒ n < m
+  | false ⇒ n ≮ m
+  ].
+intros;
+unfold ltb;
+apply leb_elim;
+apply eqb_elim;
+intros;
+simplify;
+[ rewrite < H;
+  apply le_to_not_lt;
+  constructor 1
+| apply (not_eq_to_le_to_lt ? ? H H1)
+| rewrite < H;
+  apply le_to_not_lt;
+  constructor 1
+| apply le_to_not_lt;
+  generalize in match (not_le_to_lt ? ? H1);
+  clear H1;
+  intro;
+  apply lt_to_le;
+  assumption
+].
+qed.
+
+theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
+(n < m → (P true)) → (n ≮ m → (P false)) →
+P (ltb n m).
+intros.
+cut
+(match (ltb n m) with
+[ true  ⇒ n < m
+| false ⇒ n ≮ m] → (P (ltb n m))).
+apply Hcut.apply ltb_to_Prop.
+elim (ltb n m).
+apply ((H H2)).
+apply ((H1 H2)).
+qed.
+
 let rec nat_compare n m: compare \def
 match n with
 [ O \Rightarrow 
@@ -203,11 +264,6 @@ nat_compare n m = nat_compare (S n) (S m).
 intros.simplify.reflexivity.
 qed.
 
-theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
-intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
-apply eq_f.apply pred_Sn.
-qed.
-
 theorem nat_compare_pred_pred: 
 \forall n,m:nat.lt O n \to lt O m \to 
 eq compare (nat_compare n m) (nat_compare (pred n) (pred m)).