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

[helm.git] / helm / software / matita / dama / depends

diff --git a/helm/software/matita/dama/depends b/helm/software/matita/dama/depends
index a047fc9d110a1b06e173fd892edf6959897bd3fb..e96472aa927e914fa867866ead5bb99728b55229 100644 (file)
--- a/helm/software/matita/dama/depends
+++ b/helm/software/matita/dama/depends
@@ -1,4 +1,4 @@
-metric_lattice.ma lattice.ma metric_space.ma
+metric_lattice.ma excess.ma lattice.ma metric_space.ma
 metric_space.ma ordered_divisible_group.ma
 sandwich.ma metric_lattice.ma nat/orders.ma nat/plus.ma sequence.ma
 premetric_lattice.ma lattice.ma metric_space.ma
@@ -7,12 +7,15 @@ divisible_group.ma group.ma nat/orders.ma
 ordered_divisible_group.ma divisible_group.ma nat/orders.ma nat/times.ma ordered_group.ma
 sequence.ma excess.ma nat/orders.ma ordered_group.ma
 constructive_connectives.ma logic/connectives.ma
+lattice.TF.ma excess.ma lattice.ma nat/nat.ma
 group.ma excess.ma
 prevalued_lattice.ma ordered_group.ma
 excess.ma constructive_connectives.ma constructive_higher_order_relations.ma higher_order_defs/relations.ma nat/plus.ma
+sandwich_corollary.ma metric_lattice.ma sandwich.ma
 Q_is_orded_divisble_group.ma Q/q.ma ordered_divisible_group.ma
 lattice.ma excess.ma
 constructive_higher_order_relations.ma constructive_connectives.ma higher_order_defs/relations.ma
+infsup.ma sandwich_corollary.ma
 constructive_pointfree/lebesgue.ma constructive_connectives.ma metric_lattice.ma sequence.ma
 classical_pointwise/topology.ma classical_pointwise/sets.ma
 classical_pointwise/sigma_algebra.ma classical_pointwise/topology.ma
@@ -25,16 +28,10 @@ attic/integration_algebras.ma attic/vector_spaces.ma lattice.ma
 attic/vector_spaces.ma attic/reals.ma
 attic/rings.ma group.ma
 attic/ordered_fields_ch0.ma group.ma attic/fields.ma ordered_group.ma
-nat/nat.ma 
-logic/connectives.ma 
-higher_order_defs/relations.ma 
 Q/q.ma 
-nat/plus.ma 
 higher_order_defs/relations.ma 
 logic/connectives.ma 
-nat/orders.ma 
-nat/times.ma 
-nat/orders.ma 
+nat/nat.ma 
 nat/orders.ma 
 nat/plus.ma 
-nat/orders.ma 
+nat/times.ma