X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fcompare.ma;h=194b38d84f255e3924a3273919f01bb96d320ca5;hb=3a12950125e7a4a792546aacea40505f3cecae89;hp=3a8e4a87ca50a7416e2df5f72920ea151977f41c;hpb=7bbce6bc163892cfd99cfcda65db42001b86789f;p=helm.git

diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index 3a8e4a87c..194b38d84 100644
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -1,5 +1,5 @@
 (**************************************************************************)
-(*       ___	                                                            *)
+(*       ___	                                                          *)
 (*      ||M||                                                             *)
 (*      ||A||       A project by Andrea Asperti                           *)
 (*      ||T||                                                             *)
@@ -18,6 +18,52 @@ include "nat/orders.ma".
 include "datatypes/bool.ma".
 include "datatypes/compare.ma".
 
+let rec eqb n m \def 
+match n with 
+  [ O \Rightarrow 
+     match m with 
+     [ O \Rightarrow true
+	   | (S q) \Rightarrow false] 
+  | (S p) \Rightarrow
+	   match m with 
+     [ O \Rightarrow false
+	   | (S q) \Rightarrow eqb p q]].
+	   
+theorem eqb_to_Prop: \forall n,m:nat. 
+match (eqb n m) with
+[ true  \Rightarrow n = m 
+| false \Rightarrow \lnot (n = m)].
+intros.
+apply nat_elim2
+(\lambda n,m:nat.match (eqb n m) with
+[ true  \Rightarrow n = m 
+| false \Rightarrow \lnot (n = m)]).
+intro.elim n1.
+simplify.reflexivity.
+simplify.apply not_eq_O_S.
+intro.
+simplify.
+intro. apply not_eq_O_S n1 ?.apply sym_eq.assumption.
+intros.simplify.
+generalize in match H.
+elim (eqb n1 m1).
+simplify.apply eq_f.apply H1.
+simplify.intro.apply H1.apply inj_S.assumption.
+qed.
+
+theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop.
+(n=m \to (P true)) \to (\lnot n=m \to (P false)) \to (P (eqb n m)). 
+intros.
+cut 
+match (eqb n m) with
+[ true  \Rightarrow n = m
+| false \Rightarrow \lnot (n = m)] \to (P (eqb n m)).
+apply Hcut.apply eqb_to_Prop.
+elim eqb n m.
+apply (H H2).
+apply (H1 H2).
+qed.
+
 let rec leb n m \def 
 match n with 
     [ O \Rightarrow true