Restructuring.

diff --git a/helm/software/matita/library/nat/div_and_mod_diseq.ma b/helm/software/matita/library/nat/div_and_mod_diseq.ma
index 4977df66053f23a656d2ae89c59b6deb77dd734a..299897a38ce7222d93e9114a84ff51e8dc815d60 100644 (file)
--- a/helm/software/matita/library/nat/div_and_mod_diseq.ma
+++ b/helm/software/matita/library/nat/div_and_mod_diseq.ma
@@ -183,10 +183,9 @@ apply le_times_r.
 assumption.
 qed.
    
-theorem lt_times_to_lt_div: \forall m,n,q. O < q \to 
-n < m*q \to n/q < m.
+theorem lt_times_to_lt_div: \forall m,n,q. n < m*q \to n/q < m.
 intros.
-apply (lt_times_to_lt q ? ? H).
+apply (lt_times_to_lt q ? ? (lt_times_to_lt_O ? ? ? H)).
 rewrite > sym_times.
 rewrite > sym_times in ⊢ (? ? %).
 apply (le_plus_to_le (n \mod q)).
@@ -197,42 +196,38 @@ rewrite < div_mod
     [assumption
     |apply le_plus_n
     ]
-  |assumption
+  |apply (lt_times_to_lt_O ? ? ? H)
   ]
 qed.
 
 theorem lt_div: \forall n,m. O < m \to S O < n \to m/n < m.
 intros.
-apply lt_times_to_lt_div
-  [apply lt_to_le. assumption
-  |rewrite > sym_times.
-   apply lt_m_nm;assumption
-  ]
+apply lt_times_to_lt_div.
+rewrite < sym_times.
+apply lt_m_nm;assumption.
 qed. 
   
 theorem le_div_plus_S: \forall m,n,q. O < q \to
 (m+n)/q \le S(m/q + n/q).
 intros.
 apply le_S_S_to_le.
-apply lt_times_to_lt_div
-  [assumption
-  |change in ⊢ (? ? %) with (q + (q + (m/q+n/q)*q)).
-   rewrite > sym_times.
-   rewrite > distr_times_plus.
-   rewrite > sym_times.
-   rewrite < assoc_plus in ⊢ (? ? (? ? %)).
-   rewrite < assoc_plus.
-   rewrite > sym_plus in ⊢ (? ? (? % ?)).
-   rewrite > assoc_plus.
-   apply lt_plus
-    [change with (m < S(m/q)*q).
-     apply lt_div_S.
-     assumption
-    |rewrite > sym_times.
-     change with (n < S(n/q)*q).
-     apply lt_div_S.
-     assumption
-    ]
+apply lt_times_to_lt_div.
+change in ⊢ (? ? %) with (q + (q + (m/q+n/q)*q)).
+rewrite > sym_times.
+rewrite > distr_times_plus.
+rewrite > sym_times.
+rewrite < assoc_plus in ⊢ (? ? (? ? %)).
+rewrite < assoc_plus.
+rewrite > sym_plus in ⊢ (? ? (? % ?)).
+rewrite > assoc_plus.
+apply lt_plus
+  [change with (m < S(m/q)*q).
+   apply lt_div_S.
+   assumption
+  |rewrite > sym_times.
+   change with (n < S(n/q)*q).
+   apply lt_div_S.
+   assumption
   ]
 qed.
 

diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma
index 249957f1b3bc44453e46caf4099361818b4cbbff..f89c32f870c6f4dfe26fd4406ce8a7079a3ea39f 100644 (file)
--- a/helm/software/matita/library/nat/generic_iter_p.ma
+++ b/helm/software/matita/library/nat/generic_iter_p.ma
@@ -14,6 +14,7 @@
 
 set "baseuri" "cic:/matita/nat/generic_iter_p".
 
+include "nat/div_and_mod_diseq.ma".
 include "nat/primes.ma".
 include "nat/ord.ma".
 
@@ -47,8 +48,6 @@ rewrite > H.
 reflexivity.
 qed.
 
-
-
 theorem false_to_iter_p_gen_Sn: 
 \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
 \forall baseA:A. \forall plusA: A \to A \to A.
@@ -59,7 +58,6 @@ rewrite > H.
 reflexivity.
 qed.
 
-
 theorem eq_iter_p_gen: \forall p1,p2:nat \to bool. \forall A:Type.
 \forall g1,g2: nat \to A. \forall baseA: A. 
 \forall plusA: A \to A \to A. \forall n:nat.
@@ -708,9 +706,38 @@ elim n
 ]
 qed.
 
-
-(* da spostare *)
-
+theorem eq_iter_p_gen_pred: 
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+\forall n,p,g.
+p O = true \to
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) \to
+iter_p_gen (S n) (\lambda i.p (pred i)) A (\lambda i.g(pred i)) baseA plusA = 
+plusA (iter_p_gen n p A g baseA plusA) (g O).
+intros.
+elim n
+  [rewrite > true_to_iter_p_gen_Sn
+    [simplify.apply H1
+    |assumption
+    ]
+  |apply (bool_elim ? (p n1));intro
+    [rewrite > true_to_iter_p_gen_Sn
+      [rewrite > true_to_iter_p_gen_Sn in ⊢ (? ? ? %)
+        [rewrite > H2 in ⊢ (? ? ? %).
+         apply eq_f.assumption
+        |assumption
+        ]
+      |assumption
+      ]
+    |rewrite > false_to_iter_p_gen_Sn
+      [rewrite > false_to_iter_p_gen_Sn in ⊢ (? ? ? %);assumption
+      |assumption
+      ]
+    ]
+  ]
+qed.
+    
 definition p_ord_times \def
 \lambda p,m,x.
   match p_ord x p with
@@ -749,23 +776,6 @@ elim (le_to_or_lt_eq O ? (le_O_n m))
   ]
 qed.
 
-(* lemmino da postare *)
-theorem lt_times_to_lt_div: \forall i,n,m. i < n*m \to i/m < n.
-intros.
-cut (O < m)
-  [apply (lt_times_n_to_lt m)
-    [assumption
-    |apply (le_to_lt_to_lt ? i)
-      [rewrite > (div_mod i m) in \vdash (? ? %).
-       apply le_plus_n_r.
-       assumption
-      |assumption
-      ]
-    ]
-  |apply (lt_times_to_lt_O ? ? ? H)
-  ]
-qed.
-
 theorem iter_p_gen_knm:
 \forall A:Type.
 \forall baseA: A.

diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma
index ea306f4554a6c2c83e809dace78d034d9534bcc8..c5236ff4a6f8678907c1143bf47ffd18d5c1dcf5 100644 (file)
--- a/helm/software/matita/library/nat/iteration2.ma
+++ b/helm/software/matita/library/nat/iteration2.ma
@@ -191,6 +191,20 @@ apply (eq_iter_p_gen_gh nat O plus ? ? ? g h h1 n n1 p1 p2)
 ]
 qed.
 
+theorem eq_sigma_p_pred: 
+\forall n,p,g. p O = true \to
+sigma_p (S n) (\lambda i.p (pred i)) (\lambda i.g(pred i)) = 
+plus (sigma_p n p g) (g O).
+intros.
+unfold sigma_p.
+apply eq_iter_p_gen_pred
+  [assumption
+  |apply symmetricIntPlus
+  |apply associative_plus
+  |intros.apply sym_eq.apply plus_n_O
+  ]
+qed.
+
 (* monotonicity *)
 theorem le_sigma_p: 
 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.

diff --git a/helm/software/matita/library/nat/lt_arith.ma b/helm/software/matita/library/nat/lt_arith.ma
index d8422a4dd5ff080a8e8de9eee45ace0f53a10a6f..b4c31c526ca8bb321902661bc89040274349b99a 100644 (file)
--- a/helm/software/matita/library/nat/lt_arith.ma
+++ b/helm/software/matita/library/nat/lt_arith.ma
@@ -118,6 +118,17 @@ apply (nat_case1 a)
 ]
 qed.
 
+lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
+intros.
+elim (le_to_or_lt_eq O ? (le_O_n m))
+  [assumption
+  |apply False_ind.
+   rewrite < H1 in H.
+   rewrite < times_n_O in H.
+   apply (not_le_Sn_O ? H)
+  ]
+qed.
+
 (* times *)
 theorem monotonic_lt_times_r: 
 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index f3db405d42f09b63c8a9378b481075934d667d59..4b90420c8f78bc913499bdc476acfffb4fbf1b14 100644 (file)
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -195,7 +195,22 @@ apply lt_sigma_p
   ]
 qed.
        
-   
+theorem le_exp_Sn_n_SSSO: \forall n. (exp (S n) n) \le (S(S(S O))).
+intro.  
+apply (trans_le ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
+  [apply le_exp_sigma_p_exp
+  |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) i))))
+    [apply le_sigma_p.intros.
+     apply le_times_to_le_div
+      [apply lt_O_exp.
+       apply lt_O_S
+      |apply (trans_le ? ((S(S O))\sup i* n \sup n/i!))
+        [apply le_times_div_div_times.
+         apply lt_O_fact
+        |apply le_times_to_le_div2
+          [apply lt_O_fact
+          |rewrite < sym_times.
+           apply le_times_r.