Some qed-

diff --git a/matita/matita/lib/arithmetics/div_and_mod.ma b/matita/matita/lib/arithmetics/div_and_mod.ma
index 4044695d221c775f833f90f212f09e7397d86942..966ea3c84bc05e34c4aa6f426e0a85369c9f0d8e 100644 (file)
--- a/matita/matita/lib/arithmetics/div_and_mod.ma
+++ b/matita/matita/lib/arithmetics/div_and_mod.ma
@@ -153,7 +153,7 @@ theorem mod_S: ∀n,m:nat. O < m → S (n \mod m) < m →
 ((S n) \mod m) = S (n \mod m).
 #n #m #posm #H 
 @(div_mod_spec_to_eq2 (S n) m … (n / m) ? (div_mod_spec_div_mod …))
-// @div_mod_spec_intro// (applyS eq_f) //
+// @div_mod_spec_intro// applyS eq_f // 
 qed.
 
 theorem mod_O_n: ∀n:nat.O \mod n = O.
@@ -177,7 +177,7 @@ theorem or_div_mod: ∀n,q. O < q →
   ((S (n \mod q)<q) ∧ S n = (div n q) * q + S (n\mod q))).
 #n #q #posq 
 (elim (le_to_or_lt_eq ?? (lt_mod_m_m n q posq))) #H
-  [%2 % // (applyS eq_f) //
+  [%2 % // applyS eq_f // 
   |%1 % // /demod/ <H in ⊢(? ? ? (? % ?)) @eq_f//
   ]
 qed.

diff --git a/matita/matita/lib/arithmetics/exp.ma b/matita/matita/lib/arithmetics/exp.ma
index 1205044be600641cfbbff9af76683e28a2530370..ff0572c82c982a1b01cc82c6f626da0be05e15bd 100644 (file)
--- a/matita/matita/lib/arithmetics/exp.ma
+++ b/matita/matita/lib/arithmetics/exp.ma
@@ -48,8 +48,54 @@ qed.
 
 theorem lt_O_exp: ∀n,m:nat. O < n → O < n^m. 
 #n #m (elim m) normalize // #a #Hind #posn 
-@(le_times 1 ? 1) /2/
-qed.
+@(le_times 1 ? 1) /2/ qed.
+
+(* [applyS monotonic_le_minus_r /2/ 
+
+> (minus_Sn_n ?) 
+[cut (∃x.∃y.∃z.(x - y ≤ x - z) = (1 ≤ n ^a))
+  [@ex_intro
+    [|@ex_intro
+      [|@ex_intro
+        [|     
+@(rewrite_r \Nopf  (S  n \sup a - n \sup a )
+ (\lambda x:\Nopf 
+  .(S  n \sup a - n \sup a \le S  n \sup a -(S ?-?))=(x\le  n \sup a ))
+ (rewrite_r \Nopf  ?
+  (\lambda x:\Nopf 
+   .(S  n \sup a - n \sup a \le x)=(S  n \sup a - n \sup a \le  n \sup a ))
+  ( refl … Type[0]  (S  n \sup a - n \sup a \le  n \sup a ) ) (S ?-(S ?-?))
+  (rewrite_r \Nopf  (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
+   (rewrite_l \Nopf  1 (\lambda x:\Nopf .S ?-x=n ^a -O) (minus_S_S ? O) (S ?-?)
+    (minus_Sn_n ?)) ?
+   (minus_n_O ?))) 1
+ (minus_Sn_n  n \sup a ))  
+         
+@(rewrite_r \Nopf  (S ?-?)
+ (\lambda x:\Nopf 
+  .(S  n \sup a - n \sup a \le S  n \sup a -(S ?-?))=(x\le  n \sup a ))
+ (rewrite_r \Nopf  ?
+  (\lambda x:\Nopf 
+   .(S  n \sup a - n \sup a \le x)=(S  n \sup a - n \sup a \le  n \sup a ))
+  ( refl ??) (S ?-(S ?-?))
+  ?) 1
+ (minus_Sn_n ?))
+  [||
+@(rewrite_r \Nopf  (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
+  ???)
+[|<(minus_Sn_n ?)
+@(rewrite_r \Nopf  (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
+ (rewrite_l \Nopf  1 (\lambda x:\Nopf .S ?-x=?-O) 
+    ? (S ?-?)
+    (minus_Sn_n ?)) ??)
+ 
+@(rewrite_r \Nopf  (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
+   (rewrite_l \Nopf  1 (\lambda x:\Nopf .S ?-x=?-O) (minus_S_S ? O) (S ?-?)
+    (minus_Sn_n ?)) ?
+   (minus_n_O ?)))
+
+applyS monotonic_le_minus_r /2/
+qed. *)
 
 theorem lt_m_exp_nm: ∀n,m:nat. 1 < n → m < n^m.
 #n #m #lt1n (elim m) normalize // 

diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma
index 4c55ea6beb9b37a91e752913a0338786cea24952..e558754d04145a8082d244f7f72ee046b723acd6 100644 (file)
--- a/matita/matita/lib/arithmetics/minimization.ma
+++ b/matita/matita/lib/arithmetics/minimization.ma
@@ -230,8 +230,8 @@ lemma min_exists: ∀f.∀t,m. m < t → f m = true →
   [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
    @lt_to_not_le //
   |#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
-    [#ltbm >false_min /2/ @Hind // 
-      [#i #H #H1 @ismin /2/ | >eqt normalize //]
+    [#ltbm >false_min /2/ @Hind //
+      [#i #H #H1 @ismin /2/ | >eqt normalize //] 
     |#eqbm >true_min //
     ]
   ]

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 6b3a1a19bf7b730af3e90aacec9d36b48a3d0289..f4d78234f7ef1a4ea3282d6f97dd343ad74354b6 100644 (file)
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -1,4 +1,4 @@
-(*
+  (*
     ||M||  This file is part of HELM, an Hypertextual, Electronic        
     ||A||  Library of Mathematics, developed at the Computer Science     
     ||T||  Department of the University of Bologna, Italy.                     
@@ -239,7 +239,7 @@ theorem monotonic_pred: monotonic ? le pred.
 
 theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
 (* demo *)
-/2/ qed.
+/2/ qed-.
 
 (* this are instances of the le versions 
 theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m.
@@ -390,7 +390,7 @@ qed. *)
 
 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
 #n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
-#Heq /3/ qed.
+#Heq /3/ qed-.
 (*
 nelim (Hneq Heq) qed. *)
 
@@ -466,7 +466,7 @@ qed.
 theorem le_n_fn: ∀f:nat → nat. 
   increasing f → ∀n:nat. n ≤ f n.
 #f #incr #n (elim n) /2/
-qed.
+qed-.
 
 theorem increasing_to_le: ∀f:nat → nat. 
   increasing f → ∀m:nat.∃i.m ≤ f i.
@@ -517,7 +517,7 @@ theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
 theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2  → m1 ≤ m2 
 → n1 + m1 ≤ n2 + m2.
 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
-/2/ qed.
+/2/ qed-.
 
 theorem le_plus_n :∀n,m:nat. m ≤ n + m.
 /2/ qed. 
@@ -532,13 +532,13 @@ theorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
 /2/ qed.
 
 theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
-// qed.
+// qed-.
 
 theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
 #a (elim a) normalize /3/ qed. 
 
 theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
-/2/ qed. 
+/2/ qed-. 
 
 (* plus & lt *)
 
@@ -566,7 +566,7 @@ theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p<q.
 /2/ qed.
 
 theorem lt_plus_to_lt_r :∀n,p,q:nat. n+p < n+q → p<q.
-/2/ qed.
+/2/ qed-.
 
 (*
 theorem le_to_lt_to_lt_plus: ∀a,b,c,d:nat.
@@ -615,7 +615,7 @@ theorem le_times_to_le:
   |#n #m #H #lta #le
      @le_S_S @H /2/
   ]
-qed.
+qed-.
 
 (*
 theorem le_S_times_2: ∀n,m.O < m → n ≤ m → S n ≤ 2*m.
@@ -719,7 +719,7 @@ qed.
 
 theorem lt_times_n_to_lt_r: 
 ∀n,p,q:nat. n*p < n*q → p < q.
-/2/ qed.
+/2/ qed-.
 
 (*
 theorem nat_compare_times_l : \forall n,p,q:nat. 
@@ -968,7 +968,7 @@ cases (decidable_le (m+p) n) #Hlt
   [@plus_to_minus @plus_to_minus <associative_plus
    @minus_to_plus //
   |cut (n ≤ m+p) [@(transitive_le … (le_n_Sn …)) @not_le_to_lt //]
-   #H >eq_minus_O /2/ >eq_minus_O // 
+   #H >eq_minus_O /2/ (* >eq_minus_O // *) 
   ]
 qed.
 
@@ -1095,7 +1095,7 @@ lemma le_minr: ∀i,n,m. i ≤ min n m → i ≤ m.
 #i #n #m normalize @leb_elim normalize /2/ qed. 
 
 lemma le_minl: ∀i,n,m. i ≤ min n m → i ≤ n.
-/2/ qed.
+/2/ qed-.
 
 lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m.
 #i #n #m #lein #leim normalize (cases (leb n m)) 
@@ -1111,7 +1111,7 @@ lemma le_maxl: ∀i,n,m. max n m ≤ i → n ≤ i.
 #i #n #m normalize @leb_elim normalize /2/ qed. 
 
 lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
-/2/ qed.
+/2/ qed-.
 
 lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
 #i #n #m #leni #lemi normalize (cases (leb n m)) 

diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index 2e2ef98fbc18a2c113ddac96aa996cc96a2debfb..c44caa7fef34bd19c77340b40a7d6111bcc85d1d 100644 (file)
--- a/matita/matita/lib/arithmetics/primes.ma
+++ b/matita/matita/lib/arithmetics/primes.ma
@@ -255,18 +255,17 @@ smallest_factor n = (min n 2 (λm.(eqb (n \mod m) O))).
 #n #lt1n normalize >lt_to_leb_false //
 qed.
 
-(* it works ! 
-theorem example1 : smallest_factor 3 = 3.
+example example1 : smallest_factor 3 = 3.
 normalize //
 qed.
 
-theorem example2: smallest_factor 4 = 2.
+example example2: smallest_factor 4 = 2.
 normalize //
 qed.
 
-theorem example3 : smallest_factor 7 = 7.
+example example3 : smallest_factor 7 = 7.
 normalize //
-qed. *)
+qed. 
 
 theorem le_SO_smallest_factor: ∀n:nat. 
   n ≤ 1 → smallest_factor n = n.
@@ -339,16 +338,16 @@ definition primeb ≝ λn:nat.
   (leb 2 n) ∧ (eqb (smallest_factor n) n).
 
 (* it works! *)
-theorem example4 : primeb 3 = true.
+example example4 : primeb 3 = true.
 normalize // qed.
 
-theorem example5 : primeb 6 = false.
+example example5 : primeb 6 = false.
 normalize // qed.
 
-theorem example6 : primeb 11 = true.
+example example6 : primeb 11 = true.
 normalize // qed.
 
-theorem example7 : primeb 17 = true.
+example example7 : primeb 17 = true.
 normalize // qed.
 
 theorem primeb_true_to_prime : ∀n:nat.
@@ -446,14 +445,14 @@ lemma nth_primeS: ∀n.nth_prime (S n) =
 // qed.
     
 (* it works *)
-theorem example11 : nth_prime 2 = 5.
+example example11 : nth_prime 2 = 5.
 normalize // qed.
 
-theorem example12: nth_prime 3 = 7.
+example example12: nth_prime 3 = 7.
 normalize //
 qed.
 
-theorem example13 : nth_prime 4 = 11.
+example example13 : nth_prime 4 = 11.
 normalize // qed.
 
 (* done in 13.1369330883s -- qualcosa non va: // lentissimo