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

[helm.git] / helm / software / matita / dama / ordered_divisible_group.ma

diff --git a/helm/software/matita/dama/ordered_divisible_group.ma b/helm/software/matita/dama/ordered_divisible_group.ma
index 34bd25a237149beffc813b51c56c7ad43d6f97b2..15dd52cdb853ba822b7d35e4a1ab959b0bf6e311 100644 (file)
--- a/helm/software/matita/dama/ordered_divisible_group.ma
+++ b/helm/software/matita/dama/ordered_divisible_group.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/ordered_divisible_group/".
+
 
 include "nat/orders.ma".
 include "nat/times.ma".
@@ -32,39 +32,44 @@ qed.
 
 coercion cic:/matita/ordered_divisible_group/todg_division.con.
 
-lemma pow_lt: ∀G:todgroup.∀x:G.∀n.0 < x → 0 < x + pow ? x n.
-intros (G x n H); elim n; [
-  simplify; apply (lt_rewr ???? (plus_comm ???)); 
-  apply (lt_rewr ???x (zero_neutral ??)); assumption]
-simplify; apply (lt_transitive ?? (x+(x)\sup(n1))); [assumption]
-apply flt_plusl; apply (lt_rewr ???? (plus_comm ???));
-apply (lt_rewl ??? (0 + (x \sup n1)) (eq_sym ??? (zero_neutral ??)));
-apply (lt_rewl ???? (plus_comm ???));
-apply flt_plusl; assumption;
-qed.
-
-lemma pow_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ pow ? x n.
+lemma mul_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ n * x.
 intros (G x n); elim n; simplify; [apply le_reflexive]
 apply (le_transitive ???? H1); 
-apply (le_rewl ??? (0+(x\sup n1)) (zero_neutral ??));
+apply (Le≪ (0+(n1*x)) (zero_neutral ??));
 apply fle_plusr; assumption;
 qed. 
 
-lemma ge_pow: ∀G:todgroup.∀x:G.∀n.0 < pow ? x n → 0 < x.
-intros 3; elim n; [
-  simplify in l; cases (lt_coreflexive ?? l);]
-simplify in l; 
-cut (0+0<x+(x)\sup(n1));[2:
-  apply (lt_rewl ??? 0 (zero_neutral ??)); assumption].
-cases (pippo4 ????? Hcut); [assumption]
+lemma lt_ltmul: ∀G:todgroup.∀x,y:G.∀n. x < y → S n * x < S n * y.
+intros; elim n; [simplify; apply flt_plusr; assumption]
+simplify; apply (ltplus); [assumption] assumption;
+qed.
+
+lemma ltmul_lt: ∀G:todgroup.∀x,y:G.∀n. S n * x < S n * y → x < y.
+intros 4; elim n; [apply (plus_cancr_lt ??? 0); assumption]
+simplify in l; cases (ltplus_orlt ????? l); [assumption]
 apply f; assumption;
 qed.
 
 lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0<e → 0 < e/n.
-intros; elim n; [apply (lt_rewr ???? (div1 ??));assumption]
+intros; elim n; [apply (Lt≫ ? (div1 ??));assumption]
 unfold divide; elim (dg_prop G e (S n1)); simplify; simplify in f;
-apply (ge_pow ?? (S (S n1))); apply (lt_rewr ???? f); assumption;
+apply (ltmul_lt ??? (S n1)); simplify; apply (Lt≫ ? f);
+apply (Lt≪ ? (zero_neutral ??)); (* bug se faccio repeat *)
+apply (Lt≪ ? (zero_neutral ??));  
+apply (Lt≪ ? (mulzero ?n1));
+assumption;
 qed.
 
-alias num (instance 0) = "natural number".
-axiom core1: ∀G:todgroup.∀e:G.0<e → e/3 + e/2 + e/2 < e.
+lemma muleqplus_lt: ∀G:todgroup.∀x,y:G.∀n,m.
+   0<x → 0<y → S n * x ≈ S (n + S m) * y → y < x.
+intros (G x y n m H1 H2 H3); apply (ltmul_lt ??? n); apply (Lt≫ ? H3);
+clear H3; elim m; [
+  rewrite > sym_plus; simplify; apply (Lt≪ (0+(y+n*y))); [
+    apply eq_sym; apply zero_neutral]
+  apply flt_plusr; assumption;]
+apply (lt_transitive ???? l); rewrite > sym_plus; simplify;  
+rewrite > (sym_plus n); simplify; repeat apply flt_plusl;
+apply (Lt≪ (0+(n1+n)*y)); [apply eq_sym; apply zero_neutral]
+apply flt_plusr; assumption;
+qed.  
+