Bertrand's conjecture (weak), some work in progress

[helm.git] / helm / software / matita / library / nat / generic_iter_p.ma

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.