dama almost ok

diff --git a/helm/software/matita/library/dama/bishop_set.ma b/helm/software/matita/library/dama/bishop_set.ma
index d69bb2732b3f1a4a023aa21bdd54fc4635c3b7b7..3fa4eda96910abbabd26842e13d948c23706d1e6 100644 (file)
--- a/helm/software/matita/library/dama/bishop_set.ma
+++ b/helm/software/matita/library/dama/bishop_set.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ordered_set.ma".
+include "dama/ordered_set.ma".
 
 (* Definition 2.2, setoid *)
 record bishop_set: Type ≝ {
@@ -86,4 +86,4 @@ notation "s 2 \atop \neq" non associative with precedence 90
 notation > "s 'squareB'" non associative with precedence 90
   for @{ 'squareB $s }.
 interpretation "bishop set square" 'squareB x = (square_bishop_set x).
-interpretation "bishop set square" 'square_bs x = (square_bishop_set x).
\ No newline at end of file
+interpretation "bishop set square" 'square_bs x = (square_bishop_set x).

diff --git a/helm/software/matita/library/dama/bishop_set_rewrite.ma b/helm/software/matita/library/dama/bishop_set_rewrite.ma
index ff063e29a0adaaeed17bb1f6d9ad0404970a082b..eaf6f65cf57a488e37a52c809ac3a1d63d2a59a4 100644 (file)
--- a/helm/software/matita/library/dama/bishop_set_rewrite.ma
+++ b/helm/software/matita/library/dama/bishop_set_rewrite.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "bishop_set.ma".
+include "dama/bishop_set.ma".
 
 coercion eq_sym.
 

diff --git a/helm/software/matita/library/dama/lebesgue.ma b/helm/software/matita/library/dama/lebesgue.ma
index f81c5ce46e452a2082062df61f48044f9c5ca870..1b3f5025de55d3b50b8fed85c1f37f793c0db69c 100644 (file)
--- a/helm/software/matita/library/dama/lebesgue.ma
+++ b/helm/software/matita/library/dama/lebesgue.ma
@@ -12,9 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* manca un pezzo del pullback, se inverto poi non tipa *)
-include "sandwich.ma".
-include "property_exhaustivity.ma".
+include "dama/sandwich.ma".
+include "dama/property_exhaustivity.ma".
 
 (* NOT DUALIZED *)
 alias symbol "low" = "lower".

diff --git a/helm/software/matita/library/dama/models/discrete_uniformity.ma b/helm/software/matita/library/dama/models/discrete_uniformity.ma
index 76461f3f46222f911f4a366a90d8360cfd9ca426..e3ece7df16c12de0ad8507b7c41826c92be6215a 100644 (file)
--- a/helm/software/matita/library/dama/models/discrete_uniformity.ma
+++ b/helm/software/matita/library/dama/models/discrete_uniformity.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "uniform.ma".
-include "bishop_set_rewrite.ma".
+include "dama/uniform.ma".
+include "dama/bishop_set_rewrite.ma".
 
 definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
 intro C; apply (mk_uniform_space C);

diff --git a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
index 58626ff158f194d539a471339a86ac09db1f4db5..4f7a2f847469050911a9861814792068f59e4cfe 100644 (file)
--- a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
+++ b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
@@ -12,10 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "models/nat_uniform.ma".
-include "supremum.ma".
+include "dama/models/nat_uniform.ma".
+include "dama/supremum.ma".
 include "nat/le_arith.ma".
-include "russell_support.ma".
+include "dama/russell_support.ma".
 
 lemma hint1:
  ∀s.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set s))

diff --git a/helm/software/matita/library/dama/models/nat_lebesgue.ma b/helm/software/matita/library/dama/models/nat_lebesgue.ma
index d5e65215ec43a4bdaa3bc18be7d10acad54555c5..8d563b1e351d469c4cb2097dda9fcd094b689915 100644 (file)
--- a/helm/software/matita/library/dama/models/nat_lebesgue.ma
+++ b/helm/software/matita/library/dama/models/nat_lebesgue.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lebesgue.ma".
-include "models/nat_order_continuous.ma".
+include "dama/lebesgue.ma".
+include "dama/models/nat_order_continuous.ma".
 
 theorem nat_lebesgue_oc:
    ∀a:sequence ℕ.∀s:‡ℕ.∀H:∀i:nat.a i ∈ s. 

diff --git a/helm/software/matita/library/dama/models/nat_order_continuous.ma b/helm/software/matita/library/dama/models/nat_order_continuous.ma
index 5f00dc338d217a855296d51c18985d6f7174467e..3901c8b76b82413971adffeb1f9ca78a15da6835 100644 (file)
--- a/helm/software/matita/library/dama/models/nat_order_continuous.ma
+++ b/helm/software/matita/library/dama/models/nat_order_continuous.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "models/increasing_supremum_stabilizes.ma".
-include "models/nat_ordered_uniform.ma".
+include "dama/models/increasing_supremum_stabilizes.ma".
+include "dama/models/nat_ordered_uniform.ma".
 
 lemma nat_us_is_oc: ∀s:‡ℕ.order_continuity (segment_ordered_uniform_space ℕ s).
 intros 3; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;

diff --git a/helm/software/matita/library/dama/models/nat_ordered_uniform.ma b/helm/software/matita/library/dama/models/nat_ordered_uniform.ma
index becbab2fbb8125be50babfe7aab04f706f71d836..cd6ddbf79b9d7f9b718ab51138d50977d2ac7441 100644 (file)
--- a/helm/software/matita/library/dama/models/nat_ordered_uniform.ma
+++ b/helm/software/matita/library/dama/models/nat_ordered_uniform.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "models/nat_uniform.ma".  
-include "bishop_set_rewrite.ma".
-include "ordered_uniform.ma".
+include "dama/models/nat_uniform.ma".  
+include "dama/bishop_set_rewrite.ma".
+include "dama/ordered_uniform.ma".
 
 definition nat_ordered_uniform_space:ordered_uniform_space.
  apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ)));

diff --git a/helm/software/matita/library/dama/models/nat_uniform.ma b/helm/software/matita/library/dama/models/nat_uniform.ma
index 0b2d4356321fa873044e3db09348b70873535763..691d15dd80a584296fcf8f0029ef445ecf6e6785 100644 (file)
--- a/helm/software/matita/library/dama/models/nat_uniform.ma
+++ b/helm/software/matita/library/dama/models/nat_uniform.ma
@@ -12,11 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "nat_ordered_set.ma".
-include "models/discrete_uniformity.ma".
+include "dama/nat_ordered_set.ma".
+include "dama/models/discrete_uniformity.ma".
 
 definition nat_uniform_space: uniform_space.
 apply (discrete_uniform_space_of_bishop_set ℕ);
 qed.
 
-interpretation "Uniform space N" 'N = nat_uniform_space.
\ No newline at end of file
+interpretation "Uniform space N" 'N = nat_uniform_space.

diff --git a/helm/software/matita/library/dama/nat_ordered_set.ma b/helm/software/matita/library/dama/nat_ordered_set.ma
index 26e2f0d2953a75ac9e3706babd7ec22a3b4f695d..a6d1ec184759495301b4b6253d4f540338389fea 100644 (file)
--- a/helm/software/matita/library/dama/nat_ordered_set.ma
+++ b/helm/software/matita/library/dama/nat_ordered_set.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "nat/compare.ma".
-include "bishop_set.ma". 
+include "dama/bishop_set.ma". 
 
 definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
 

diff --git a/helm/software/matita/library/dama/ordered_uniform.ma b/helm/software/matita/library/dama/ordered_uniform.ma
index 5a712f127fa5eee5cd7ddf5e4540961cffb9207e..99bcbbf050c1cac7c4bdd054fed79f40e047a434 100644 (file)
--- a/helm/software/matita/library/dama/ordered_uniform.ma
+++ b/helm/software/matita/library/dama/ordered_uniform.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "uniform.ma".
+include "dama/uniform.ma".
 
 record ordered_uniform_space_ : Type ≝ {
   ous_os:> ordered_set;

diff --git a/helm/software/matita/library/dama/property_exhaustivity.ma b/helm/software/matita/library/dama/property_exhaustivity.ma
index deddf88049f5e60a2108942506b67a65bf79bf80..4dec6442e0fd8e26ae995e3de4ef045968a014c1 100644 (file)
--- a/helm/software/matita/library/dama/property_exhaustivity.ma
+++ b/helm/software/matita/library/dama/property_exhaustivity.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ordered_uniform.ma".
-include "property_sigma.ma".
+include "dama/ordered_uniform.ma".
+include "dama/property_sigma.ma".
 
 lemma h_segment_upperbound:
   ∀C:half_ordered_set.

diff --git a/helm/software/matita/library/dama/property_sigma.ma b/helm/software/matita/library/dama/property_sigma.ma
index 74f03de4c9fe2ee552a207c79b15c5413fe85962..26ffd59bc38d366e802f98f48a57150b60793448 100644 (file)
--- a/helm/software/matita/library/dama/property_sigma.ma
+++ b/helm/software/matita/library/dama/property_sigma.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ordered_uniform.ma".
-include "russell_support.ma".
+include "dama/ordered_uniform.ma".
+include "dama/russell_support.ma".
 
 (* Definition 3.5 *)
 alias num (instance 0) = "natural number".

diff --git a/helm/software/matita/library/dama/sandwich.ma b/helm/software/matita/library/dama/sandwich.ma
index 68bb4453cda61ce94e5aace6e3a40a8994ea3302..f8aabd472615281fa2a2cb78f2d5fb7723ac5704 100644 (file)
--- a/helm/software/matita/library/dama/sandwich.ma
+++ b/helm/software/matita/library/dama/sandwich.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ordered_uniform.ma".
+include "dama/ordered_uniform.ma".
 
 lemma le_w_plus: ∀n,m,o.n+m≤o → m ≤ o.
 intro; elim n; simplify; [assumption]

diff --git a/helm/software/matita/library/dama/supremum.ma b/helm/software/matita/library/dama/supremum.ma
index 0de61b292fcaca3e40f5b7bddfa7ba0b88d27398..be8495970a737e9f926066f381c134b7a9784dd0 100644 (file)
--- a/helm/software/matita/library/dama/supremum.ma
+++ b/helm/software/matita/library/dama/supremum.ma
@@ -15,8 +15,8 @@
 
 include "datatypes/constructors.ma".
 include "nat/plus.ma".
-include "nat_ordered_set.ma".
-include "sequence.ma".
+include "dama/nat_ordered_set.ma".
+include "dama/sequence.ma".
 
 (* Definition 2.4 *)
 definition upper_bound ≝ 

diff --git a/helm/software/matita/library/dama/uniform.ma b/helm/software/matita/library/dama/uniform.ma
index 759037124310076d813c711ea272eb323d2d6ffc..072849bd4082bbb71a6239504df63689dc7895eb 100644 (file)
--- a/helm/software/matita/library/dama/uniform.ma
+++ b/helm/software/matita/library/dama/uniform.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "supremum.ma".
+include "dama/supremum.ma".
 
 (* Definition 2.13 *)
 alias symbol "pair" = "Pair construction".

diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index f98e795f219b0966b8d395954edbf4c9e975dba6..d510318df759096dbfcdf61799742567c9396ae9 100644 (file)
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -1,11 +1,14 @@
 formal_topology/formal_topologies.ma formal_topology/basic_topologies.ma
 demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma
+dama/sandwich.ma dama/ordered_uniform.ma
 Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma
 demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma
 nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma
+dama/ordered_uniform.ma dama/uniform.ma
 nat/lt_arith.ma nat/div_and_mod.ma
 demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma
 Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma
+dama/models/nat_order_continuous.ma dama/models/increasing_supremum_stabilizes.ma dama/models/nat_ordered_uniform.ma
 nat/factorial2.ma nat/exp.ma nat/factorial.ma
 nat/orders.ma higher_order_defs/ordering.ma logic/connectives.ma nat/nat.ma
 nat/sieve.ma list/sort.ma nat/primes.ma
@@ -13,20 +16,24 @@ technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic
 nat/div_and_mod_diseq.ma nat/lt_arith.ma
 logic/cprop_connectives.ma logic/connectives.ma
 algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma
-nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
 formal_topology/saturations_reductions.ma datatypes/subsets.ma
+nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
 Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma
 nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma
-list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
 datatypes/compare.ma 
+list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
+dama/models/nat_uniform.ma dama/models/discrete_uniformity.ma dama/nat_ordered_set.ma
 didactic/exercises/substitution.ma nat/minus.ma
+didactic/exercises/natural_deduction_fst_order.ma didactic/support/natural_deduction.ma
 nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma
 formal_topology/basic_topologies.ma datatypes/categories.ma formal_topology/relations.ma formal_topology/saturations_reductions.ma
+dama/models/increasing_supremum_stabilizes.ma dama/models/nat_uniform.ma dama/russell_support.ma dama/supremum.ma nat/le_arith.ma
 logic/connectives.ma 
 Q/nat_fact/times.ma nat/factorization.ma
 decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma
 didactic/exercises/duality.ma nat/minus.ma
 nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma
+dama/supremum.ma dama/nat_ordered_set.ma dama/sequence.ma datatypes/constructors.ma nat/plus.ma
 nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma
 nat/times.ma nat/plus.ma
 nat/chebyshev_thm.ma nat/neper.ma
@@ -35,18 +42,21 @@ demo/cantor.ma datatypes/constructors.ma demo/formal_topology.ma
 nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma
 nat/le_arith.ma nat/orders.ma nat/times.ma
 decidable_kit/fgraph.ma decidable_kit/fintype.ma
+dama/models/nat_ordered_uniform.ma dama/bishop_set_rewrite.ma dama/models/nat_uniform.ma dama/ordered_uniform.ma
+dama/bishop_set.ma dama/ordered_set.ma
 nat/euler_theorem.ma nat/map_iter_p.ma nat/nat.ma nat/totient.ma
 Q/fraction/ftimes.ma Q/fraction/finv.ma Q/nat_fact/times.ma Q/ratio/ratio.ma Z/times.ma
 nat/factorial.ma nat/le_arith.ma
 Z/plus.ma Z/z.ma nat/minus.ma
 Q/ratio/rinv.ma Q/fraction/finv.ma Q/ratio/ratio.ma
 decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma
+dama/ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma
 nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
 Q/q/qplus.ma nat/factorization.ma
 decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma
+Z/orders.ma Z/z.ma nat/orders.ma
 nat/map_iter_p.ma nat/count.ma nat/permutation.ma
 Q/q.ma Q/fraction/fraction.ma Z/compare.ma Z/plus.ma nat/factorization.ma
-Z/orders.ma Z/z.ma nat/orders.ma
 nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma
 demo/realisability.ma datatypes/constructors.ma logic/connectives.ma
 list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma
@@ -66,50 +76,61 @@ algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma
 decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma
 nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma
 algebra/semigroups.ma higher_order_defs/functions.ma
+dama/models/discrete_uniformity.ma dama/bishop_set_rewrite.ma dama/uniform.ma
+dama/lebesgue.ma dama/ordered_set.ma dama/property_exhaustivity.ma dama/sandwich.ma
+formal_topology/relations.ma datatypes/subsets.ma
 higher_order_defs/relations.ma logic/connectives.ma
 nat/factorization.ma nat/ord.ma
-formal_topology/relations.ma datatypes/subsets.ma
 nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma
 Z/moebius.ma Z/sigma_p.ma nat/factorization.ma
 demo/toolbox.ma logic/cprop_connectives.ma
-logic/coimplication.ma logic/connectives.ma
 nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
+logic/coimplication.ma logic/connectives.ma
 nat/minimization.ma nat/minus.ma
 logic/connectives2.ma higher_order_defs/relations.ma
 datatypes/subsets.ma datatypes/categories.ma logic/cprop_connectives.ma
 nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/o.ma nat/pi_p.ma
 decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma
 Q/q/q.ma Q/fraction/numerator_denominator.ma Q/ratio/ratio.ma
+dama/models/nat_lebesgue.ma dama/lebesgue.ma dama/models/nat_order_continuous.ma
 nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sieve.ma nat/sqrt.ma
 nat/nat.ma higher_order_defs/functions.ma
 Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
+dama/uniform.ma dama/supremum.ma
 demo/natural_deduction.ma didactic/support/natural_deduction.ma
 higher_order_defs/ordering.ma logic/equality.ma
-logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma
 nat/congruence.ma nat/primes.ma nat/relevant_equations.ma
-nat/gcd.ma nat/lt_arith.ma nat/primes.ma
-datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma
+logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma
+dama/property_exhaustivity.ma dama/ordered_uniform.ma dama/property_sigma.ma
 Z/compare.ma Z/orders.ma nat/compare.ma
+datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma
+nat/gcd.ma nat/lt_arith.ma nat/primes.ma
+Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma
 algebra/monoids.ma algebra/semigroups.ma
 nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma
-Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma
 nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma
 datatypes/categories.ma logic/cprop_connectives.ma
 nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma
+dama/nat_ordered_set.ma nat/orders.ma dama/bishop_set.ma nat/compare.ma
 Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma
+dama/russell_support.ma logic/cprop_connectives.ma nat/nat.ma
 nat/binomial.ma nat/factorial2.ma nat/iteration2.ma
 nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma
 higher_order_defs/functions.ma logic/equality.ma
 Q/fraction/numerator_denominator.ma Q/fraction/finv.ma
-nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma
 datatypes/constructors.ma logic/equality.ma
+nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma
 nat/plus.ma nat/nat.ma
 Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma
+dama/sequence.ma nat/nat.ma
 nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma
 nat/gcd_properties1.ma nat/gcd.ma
 list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma
 didactic/exercises/natural_deduction.ma didactic/support/natural_deduction.ma
+dama/models/list_support.ma nat/le_arith.ma list/list.ma logic/cprop_connectives.ma nat/minus.ma
+dama/bishop_set_rewrite.ma dama/bishop_set.ma
 Z/times.ma Z/plus.ma nat/lt_arith.ma
 Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
 nat/o.ma nat/binomial.ma nat/sqrt.ma
+dama/property_sigma.ma dama/ordered_uniform.ma dama/russell_support.ma
 Q/inv.ma Q/fraction/finv.ma Q/q/q.ma Q/q.ma