X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Farithmetics%2Fnat.ma;h=d4ba1135e241626f551b5bca4b55c0a43f7d01e5;hb=a4cd6a8a1d6a008518c12daca794b9e811c1dee5;hp=54ff253c22404a443b6a39879aebf9211f1873f4;hpb=81e3d11cbb2a7a6498b4b19876bbb5ababc8942b;p=helm.git

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index 54ff253c2..d4ba1135e 100644
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* include "higher_order_defs/functions.ma". *)
 include "hints_declaration.ma".
 include "basics/functions.ma".
 include "basics/eq.ma".
@@ -80,7 +79,7 @@ ntheorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
 napply nat_elim2; #n;
  ##[ ncases n; /2/;
  ##| /3/;
- ##| #m; #Hind; ncases Hind; /3/;
+ ##| #m; #Hind; ncases Hind;/3/;
  ##]
 nqed. 
 
@@ -124,7 +123,7 @@ ntheorem associative_plus : associative nat plus.
 #n; nelim n; nnormalize; //; nqed.
 
 ntheorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
-//; nqed.
+//; nqed. 
 
 ntheorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
 #n; nelim n; nnormalize; /3/; nqed.
@@ -273,8 +272,6 @@ ntheorem monotonic_pred: monotonic ? le pred.
 #n; #m; #lenm; nelim lenm; /2/;nqed.
 
 ntheorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
-(* XXX *) nletin hint ≝ monotonic. 
-#a; #b; #H; napplyS monotonic_pred;
 /2/; nqed.
 
 (* this are instances of the le versions 
@@ -450,7 +447,8 @@ ntheorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m →
 (* le and eq *)
 
 ntheorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
-napply nat_elim2; /4/; nqed. 
+napply nat_elim2; /4/;
+nqed. 
 
 ntheorem lt_O_S : ∀n:nat. O < S n.
 /2/; nqed.
@@ -886,7 +884,7 @@ ntheorem minus_plus_m_m: ∀n,m:nat.n = (n+m)-m.
 
 ntheorem plus_minus_m_m: ∀n,m:nat.
   m ≤ n → n = (n-m)+m.
-#n; #m; #lemn; napplyS symmetric_eq; 
+#n; #m; #lemn; napplyS sym_eq; 
 napplyS (plus_minus m n m); //; nqed.
 
 ntheorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m.
@@ -905,7 +903,7 @@ nqed.
 ntheorem plus_to_minus :∀n,m,p:nat.n = m+p → n-m = p.
 (* /4/ done in 43.5 *)
 #n; #m; #p; #eqp; 
-napply symmetric_eq;
+napply sym_eq;
 napplyS (minus_plus_m_m p m);
 nqed.
 
@@ -1045,15 +1043,14 @@ simplify.unfold Not.intro.apply H1.apply inj_S.assumption.
 qed.
 *)
 
-naxiom eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
+ntheorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). 
-(*
 napply nat_elim2; 
   ##[#n; ncases n; nnormalize; /3/; 
   ##|nnormalize; /3/;
   ##|nnormalize; /4/; 
   ##] 
-nqed.*)
+nqed.
 
 ntheorem eqb_n_n: ∀n. eqb n n = true.
 #n; nelim n; nnormalize; //.