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

[helm.git] / helm / software / matita / dama / classical_pointfree / ordered_sets.ma

diff --git a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma
index 127bbf69623e8830c0f380983c2f375989491b0c..2630da77c6474b93a99281982f1edc229ff27ae8 100644 (file)
--- a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma
+++ b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma
@@ -12,11 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/classical_pointwise/ordered_sets/".
 
-include "ordered_set.ma".
 
-record is_dedekind_sigma_complete (O:ordered_set) : Type ≝
+include "excess.ma".
+
+record is_dedekind_sigma_complete (O:excess) : Type ≝
  { dsc_inf: ∀a:nat→O.∀m:O. is_lower_bound ? a m → ex ? (λs:O.is_inf O a s);
    dsc_inf_proof_irrelevant:
     ∀a:nat→O.∀m,m':O.∀p:is_lower_bound ? a m.∀p':is_lower_bound ? a m'.
@@ -30,7 +30,7 @@ record is_dedekind_sigma_complete (O:ordered_set) : Type ≝
  }.
 
 record dedekind_sigma_complete_ordered_set : Type ≝
- { dscos_ordered_set:> ordered_set;
+ { dscos_ordered_set:> excess;
    dscos_dedekind_sigma_complete_properties:>
     is_dedekind_sigma_complete dscos_ordered_set
  }.
@@ -155,7 +155,7 @@ lemma inf_respects_le:
 qed. 
 
 definition is_sequentially_monotone ≝
- λO:ordered_set.λf:O→O.
+ λO:excess.λf:O→O.
   ∀a:nat→O.∀p:is_increasing ? a.
    is_increasing ? (λi.f (a i)).
 
@@ -320,10 +320,10 @@ notation "hvbox(〈a〉)"
 for @{ 'hide_everything_but $a }.
 
 interpretation "mk_bounded_above_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_set/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
 
 interpretation "mk_bounded_below_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_set/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
 
 theorem eq_f_sup_sup_f:
  ∀O':dedekind_sigma_complete_ordered_set.