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

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

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 53c59de3570ca25882047244ac0a1103361671da..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.
 
@@ -306,3 +301,41 @@ apply (trans_le ? ((a*m/i)/m))
   ]
 qed.
        
+theorem le_div_times_Sm: \forall a,i,m. O < i \to O < m \to
+a / i \le (a * S (m / i))/m.
+intros.
+apply (trans_le ? ((a * S (m / i))/((S (m/i))*i)))
+  [rewrite < (eq_div_div_div_times ? i)
+    [rewrite > lt_O_to_div_times
+      [apply le_n
+      |apply lt_O_S
+      ]
+    |apply lt_O_S
+    |assumption
+    ]
+  |apply le_times_to_le_div
+    [assumption
+    |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i)))
+      [apply le_times_div_div_times.
+       rewrite > (times_n_O O).
+       apply lt_times
+        [apply lt_O_S
+        |assumption
+        ]
+      |rewrite > sym_times.
+       apply le_times_to_le_div2
+        [rewrite > (times_n_O O).
+         apply lt_times
+          [apply lt_O_S
+          |assumption
+          ]
+        |apply le_times_r.
+         apply lt_to_le.
+         apply lt_div_S.
+         assumption
+        ]
+      ]
+    ]
+  ]
+qed.
+