From 1b839e0367f89503398442b7990fb6b6d1fa2152 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 20 Apr 2007 12:26:16 +0000
Subject: [PATCH] added library_auto/ to tests.

---
 matita/Makefile                               |  1 +
 matita/library_auto/{ => auto}/Q/q.ma         |  4 +-
 matita/library_auto/{ => auto}/Z/compare.ma   |  4 +-
 matita/library_auto/{ => auto}/Z/orders.ma    |  4 +-
 matita/library_auto/{ => auto}/Z/plus.ma      |  4 +-
 matita/library_auto/{ => auto}/Z/times.ma     |  4 +-
 matita/library_auto/{ => auto}/Z/z.ma         |  2 +-
 .../{ => auto}/nat/chinese_reminder.ma        |  8 ++--
 matita/library_auto/{ => auto}/nat/compare.ma |  2 +-
 .../library_auto/{ => auto}/nat/congruence.ma |  4 +-
 matita/library_auto/{ => auto}/nat/count.ma   |  6 +--
 .../{ => auto}/nat/div_and_mod.ma             |  2 +-
 .../{ => auto}/nat/euler_theorem.ma           |  4 +-
 matita/library_auto/{ => auto}/nat/exp.ma     |  2 +-
 .../library_auto/{ => auto}/nat/factorial.ma  |  2 +-
 .../{ => auto}/nat/factorization.ma           |  6 +--
 .../{ => auto}/nat/fermat_little_theorem.ma   |  8 ++--
 matita/library_auto/{ => auto}/nat/gcd.ma     |  2 +-
 .../library_auto/{ => auto}/nat/le_arith.ma   |  4 +-
 .../library_auto/{ => auto}/nat/lt_arith.ma   |  2 +-
 .../library_auto/{ => auto}/nat/map_iter_p.ma |  4 +-
 .../{ => auto}/nat/minimization.ma            |  2 +-
 matita/library_auto/{ => auto}/nat/minus.ma   |  4 +-
 matita/library_auto/{ => auto}/nat/nat.ma     |  0
 .../library_auto/{ => auto}/nat/nth_prime.ma  |  4 +-
 matita/library_auto/{ => auto}/nat/ord.ma     |  8 ++--
 matita/library_auto/{ => auto}/nat/orders.ma  |  2 +-
 .../{ => auto}/nat/permutation.ma             |  4 +-
 matita/library_auto/{ => auto}/nat/plus.ma    |  2 +-
 matita/library_auto/{ => auto}/nat/primes.ma  |  8 ++--
 .../{ => auto}/nat/relevant_equations.ma      |  6 +--
 .../{ => auto}/nat/sigma_and_pi.ma            |  6 +--
 matita/library_auto/{ => auto}/nat/times.ma   |  2 +-
 matita/library_auto/{ => auto}/nat/totient.ma |  4 +-
 matita/library_auto/makefile                  | 39 +++++++++++++++++++
 35 files changed, 105 insertions(+), 65 deletions(-)
 rename matita/library_auto/{ => auto}/Q/q.ma (99%)
 rename matita/library_auto/{ => auto}/Z/compare.ma (98%)
 rename matita/library_auto/{ => auto}/Z/orders.ma (98%)
 rename matita/library_auto/{ => auto}/Z/plus.ma (99%)
 rename matita/library_auto/{ => auto}/Z/times.ma (99%)
 rename matita/library_auto/{ => auto}/Z/z.ma (99%)
 rename matita/library_auto/{ => auto}/nat/chinese_reminder.ma (98%)
 rename matita/library_auto/{ => auto}/nat/compare.ma (99%)
 rename matita/library_auto/{ => auto}/nat/congruence.ma (98%)
 rename matita/library_auto/{ => auto}/nat/count.ma (98%)
 rename matita/library_auto/{ => auto}/nat/div_and_mod.ma (99%)
 rename matita/library_auto/{ => auto}/nat/euler_theorem.ma (99%)
 rename matita/library_auto/{ => auto}/nat/exp.ma (99%)
 rename matita/library_auto/{ => auto}/nat/factorial.ma (98%)
 rename matita/library_auto/{ => auto}/nat/factorization.ma (99%)
 rename matita/library_auto/{ => auto}/nat/fermat_little_theorem.ma (98%)
 rename matita/library_auto/{ => auto}/nat/gcd.ma (99%)
 rename matita/library_auto/{ => auto}/nat/le_arith.ma (98%)
 rename matita/library_auto/{ => auto}/nat/lt_arith.ma (99%)
 rename matita/library_auto/{ => auto}/nat/map_iter_p.ma (99%)
 rename matita/library_auto/{ => auto}/nat/minimization.ma (99%)
 rename matita/library_auto/{ => auto}/nat/minus.ma (99%)
 rename matita/library_auto/{ => auto}/nat/nat.ma (100%)
 rename matita/library_auto/{ => auto}/nat/nth_prime.ma (99%)
 rename matita/library_auto/{ => auto}/nat/ord.ma (98%)
 rename matita/library_auto/{ => auto}/nat/orders.ma (99%)
 rename matita/library_auto/{ => auto}/nat/permutation.ma (99%)
 rename matita/library_auto/{ => auto}/nat/plus.ma (98%)
 rename matita/library_auto/{ => auto}/nat/primes.ma (99%)
 rename matita/library_auto/{ => auto}/nat/relevant_equations.ma (95%)
 rename matita/library_auto/{ => auto}/nat/sigma_and_pi.ma (97%)
 rename matita/library_auto/{ => auto}/nat/times.ma (99%)
 rename matita/library_auto/{ => auto}/nat/totient.ma (98%)
 create mode 100644 matita/library_auto/makefile

diff --git a/matita/Makefile b/matita/Makefile
index 1b73fe2da..6f62f2546 100644
--- a/matita/Makefile
+++ b/matita/Makefile
@@ -210,6 +210,7 @@ distclean: clean
 TEST_DIRS = 				\
 	legacy                          \
 	library 			\
+	library_auto 			\
 	tests 				\
 	dama				\
 	contribs/CoRN	 	        \
diff --git a/matita/library_auto/Q/q.ma b/matita/library_auto/auto/Q/q.ma
similarity index 99%
rename from matita/library_auto/Q/q.ma
rename to matita/library_auto/auto/Q/q.ma
index d78400ea0..225d68b4e 100644
--- a/matita/library_auto/Q/q.ma
+++ b/matita/library_auto/auto/Q/q.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/library_auto/Q/q".
 
-include "Z/compare.ma".
-include "Z/plus.ma".
+include "auto/Z/compare.ma".
+include "auto/Z/plus.ma".
 
 (* a fraction is a list of Z-coefficients for primes, in natural
 order. The last coefficient must eventually be different from 0 *)
diff --git a/matita/library_auto/Z/compare.ma b/matita/library_auto/auto/Z/compare.ma
similarity index 98%
rename from matita/library_auto/Z/compare.ma
rename to matita/library_auto/auto/Z/compare.ma
index c57e16672..f3bf12cb2 100644
--- a/matita/library_auto/Z/compare.ma
+++ b/matita/library_auto/auto/Z/compare.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/library_auto/Z/compare".
 
-include "Z/orders.ma".
-include "nat/compare.ma".
+include "auto/Z/orders.ma".
+include "auto/nat/compare.ma".
 
 (* boolean equality *)
 definition eqZb : Z \to Z \to bool \def
diff --git a/matita/library_auto/Z/orders.ma b/matita/library_auto/auto/Z/orders.ma
similarity index 98%
rename from matita/library_auto/Z/orders.ma
rename to matita/library_auto/auto/Z/orders.ma
index 4e912bb65..c6710e97e 100644
--- a/matita/library_auto/Z/orders.ma
+++ b/matita/library_auto/auto/Z/orders.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/library_auto/Z/orders".
 
-include "Z/z.ma".
-include "nat/orders.ma".
+include "auto/Z/z.ma".
+include "auto/nat/orders.ma".
 
 definition Zle : Z \to Z \to Prop \def
 \lambda x,y:Z.
diff --git a/matita/library_auto/Z/plus.ma b/matita/library_auto/auto/Z/plus.ma
similarity index 99%
rename from matita/library_auto/Z/plus.ma
rename to matita/library_auto/auto/Z/plus.ma
index 3cadd81d3..20d6cdb51 100644
--- a/matita/library_auto/Z/plus.ma
+++ b/matita/library_auto/auto/Z/plus.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/library_auto/Z/plus".
 
-include "Z/z.ma".
-include "nat/minus.ma".
+include "auto/Z/z.ma".
+include "auto/nat/minus.ma".
 
 definition Zplus :Z \to Z \to Z \def
 \lambda x,y.
diff --git a/matita/library_auto/Z/times.ma b/matita/library_auto/auto/Z/times.ma
similarity index 99%
rename from matita/library_auto/Z/times.ma
rename to matita/library_auto/auto/Z/times.ma
index e80828ae9..a95dc4e27 100644
--- a/matita/library_auto/Z/times.ma
+++ b/matita/library_auto/auto/Z/times.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/library_auto/Z/times".
 
-include "nat/lt_arith.ma".
-include "Z/plus.ma".
+include "auto/nat/lt_arith.ma".
+include "auto/Z/plus.ma".
 
 definition Ztimes :Z \to Z \to Z \def
 \lambda x,y.
diff --git a/matita/library_auto/Z/z.ma b/matita/library_auto/auto/Z/z.ma
similarity index 99%
rename from matita/library_auto/Z/z.ma
rename to matita/library_auto/auto/Z/z.ma
index c628064b3..a66f3c5dc 100644
--- a/matita/library_auto/Z/z.ma
+++ b/matita/library_auto/auto/Z/z.ma
@@ -15,7 +15,7 @@
 set "baseuri" "cic:/matita/library_auto/Z/z".
 
 include "datatypes/bool.ma".
-include "nat/nat.ma".
+include "auto/nat/nat.ma".
 
 inductive Z : Set \def
   OZ : Z
diff --git a/matita/library_auto/nat/chinese_reminder.ma b/matita/library_auto/auto/nat/chinese_reminder.ma
similarity index 98%
rename from matita/library_auto/nat/chinese_reminder.ma
rename to matita/library_auto/auto/nat/chinese_reminder.ma
index ae02688a0..844d949d4 100644
--- a/matita/library_auto/nat/chinese_reminder.ma
+++ b/matita/library_auto/auto/nat/chinese_reminder.ma
@@ -14,10 +14,10 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/chinese_reminder".
 
-include "nat/exp.ma".
-include "nat/gcd.ma".
-include "nat/permutation.ma".
-include "nat/congruence.ma".
+include "auto/nat/exp.ma".
+include "auto/nat/gcd.ma".
+include "auto/nat/permutation.ma".
+include "auto/nat/congruence.ma".
 
 theorem and_congruent_congruent: \forall m,n,a,b:nat. O < n \to O < m \to 
 gcd n m = (S O) \to ex nat (\lambda x. congruent x a m \land congruent x b n).
diff --git a/matita/library_auto/nat/compare.ma b/matita/library_auto/auto/nat/compare.ma
similarity index 99%
rename from matita/library_auto/nat/compare.ma
rename to matita/library_auto/auto/nat/compare.ma
index 4c432296e..bf43ef6a9 100644
--- a/matita/library_auto/nat/compare.ma
+++ b/matita/library_auto/auto/nat/compare.ma
@@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/library_auto/nat/compare".
 
 include "datatypes/bool.ma".
 include "datatypes/compare.ma".
-include "nat/orders.ma".
+include "auto/nat/orders.ma".
 
 let rec eqb n m \def 
 match n with 
diff --git a/matita/library_auto/nat/congruence.ma b/matita/library_auto/auto/nat/congruence.ma
similarity index 98%
rename from matita/library_auto/nat/congruence.ma
rename to matita/library_auto/auto/nat/congruence.ma
index 73daf90f6..606fdfcf8 100644
--- a/matita/library_auto/nat/congruence.ma
+++ b/matita/library_auto/auto/nat/congruence.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/congruence".
 
-include "nat/relevant_equations.ma".
-include "nat/primes.ma".
+include "auto/nat/relevant_equations.ma".
+include "auto/nat/primes.ma".
 
 definition S_mod: nat \to nat \to nat \def
 \lambda n,m:nat. (S m) \mod n.
diff --git a/matita/library_auto/nat/count.ma b/matita/library_auto/auto/nat/count.ma
similarity index 98%
rename from matita/library_auto/nat/count.ma
rename to matita/library_auto/auto/nat/count.ma
index 8a96d23f1..e7c0ac619 100644
--- a/matita/library_auto/nat/count.ma
+++ b/matita/library_auto/auto/nat/count.ma
@@ -14,9 +14,9 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/count".
 
-include "nat/relevant_equations.ma".
-include "nat/sigma_and_pi.ma".
-include "nat/permutation.ma".
+include "auto/nat/relevant_equations.ma".
+include "auto/nat/sigma_and_pi.ma".
+include "auto/nat/permutation.ma".
 
 theorem sigma_f_g : \forall n,m:nat.\forall f,g:nat \to nat.
 sigma n (\lambda p.f p + g p) m = sigma n f m + sigma n g m.
diff --git a/matita/library_auto/nat/div_and_mod.ma b/matita/library_auto/auto/nat/div_and_mod.ma
similarity index 99%
rename from matita/library_auto/nat/div_and_mod.ma
rename to matita/library_auto/auto/nat/div_and_mod.ma
index a2e83d1a0..9b9be7cf2 100644
--- a/matita/library_auto/nat/div_and_mod.ma
+++ b/matita/library_auto/auto/nat/div_and_mod.ma
@@ -15,7 +15,7 @@
 set "baseuri" "cic:/matita/library_auto/nat/div_and_mod".
 
 include "datatypes/constructors.ma".
-include "nat/minus.ma".
+include "auto/nat/minus.ma".
 
 let rec mod_aux p m n: nat \def
 match (leb m n) with
diff --git a/matita/library_auto/nat/euler_theorem.ma b/matita/library_auto/auto/nat/euler_theorem.ma
similarity index 99%
rename from matita/library_auto/nat/euler_theorem.ma
rename to matita/library_auto/auto/nat/euler_theorem.ma
index 0ccc4d0af..8d16ac723 100644
--- a/matita/library_auto/nat/euler_theorem.ma
+++ b/matita/library_auto/auto/nat/euler_theorem.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/euler_theorem".
 
-include "nat/map_iter_p.ma".
-include "nat/totient.ma".
+include "auto/nat/map_iter_p.ma".
+include "auto/nat/totient.ma".
 
 (* a reformulation of totient using card insted of count *)
 lemma totient_card: \forall n. 
diff --git a/matita/library_auto/nat/exp.ma b/matita/library_auto/auto/nat/exp.ma
similarity index 99%
rename from matita/library_auto/nat/exp.ma
rename to matita/library_auto/auto/nat/exp.ma
index 12c132186..f7d125541 100644
--- a/matita/library_auto/nat/exp.ma
+++ b/matita/library_auto/auto/nat/exp.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/exp".
 
-include "nat/div_and_mod.ma".
+include "auto/nat/div_and_mod.ma".
 
 let rec exp n m on m\def 
  match m with 
diff --git a/matita/library_auto/nat/factorial.ma b/matita/library_auto/auto/nat/factorial.ma
similarity index 98%
rename from matita/library_auto/nat/factorial.ma
rename to matita/library_auto/auto/nat/factorial.ma
index dedf1767f..cb0c072ed 100644
--- a/matita/library_auto/nat/factorial.ma
+++ b/matita/library_auto/auto/nat/factorial.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/factorial".
 
-include "nat/le_arith.ma".
+include "auto/nat/le_arith.ma".
 
 let rec fact n \def
   match n with 
diff --git a/matita/library_auto/nat/factorization.ma b/matita/library_auto/auto/nat/factorization.ma
similarity index 99%
rename from matita/library_auto/nat/factorization.ma
rename to matita/library_auto/auto/nat/factorization.ma
index 590683e7b..073318f9e 100644
--- a/matita/library_auto/nat/factorization.ma
+++ b/matita/library_auto/auto/nat/factorization.ma
@@ -14,9 +14,9 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/factorization".
 
-include "nat/ord.ma".
-include "nat/gcd.ma".
-include "nat/nth_prime.ma".
+include "auto/nat/ord.ma".
+include "auto/nat/gcd.ma".
+include "auto/nat/nth_prime.ma".
 
 (* the following factorization algorithm looks for the largest prime
    factor. *)
diff --git a/matita/library_auto/nat/fermat_little_theorem.ma b/matita/library_auto/auto/nat/fermat_little_theorem.ma
similarity index 98%
rename from matita/library_auto/nat/fermat_little_theorem.ma
rename to matita/library_auto/auto/nat/fermat_little_theorem.ma
index 9adb75a41..df8aff727 100644
--- a/matita/library_auto/nat/fermat_little_theorem.ma
+++ b/matita/library_auto/auto/nat/fermat_little_theorem.ma
@@ -14,10 +14,10 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/fermat_little_theorem".
 
-include "nat/exp.ma".
-include "nat/gcd.ma".
-include "nat/permutation.ma".
-include "nat/congruence.ma".
+include "auto/nat/exp.ma".
+include "auto/nat/gcd.ma".
+include "auto/nat/permutation.ma".
+include "auto/nat/congruence.ma".
 
 theorem permut_S_mod: \forall n:nat. permut (S_mod (S n)) n.
 intro.
diff --git a/matita/library_auto/nat/gcd.ma b/matita/library_auto/auto/nat/gcd.ma
similarity index 99%
rename from matita/library_auto/nat/gcd.ma
rename to matita/library_auto/auto/nat/gcd.ma
index 297196ccb..ae59700c4 100644
--- a/matita/library_auto/nat/gcd.ma
+++ b/matita/library_auto/auto/nat/gcd.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/gcd".
 
-include "nat/primes.ma".
+include "auto/nat/primes.ma".
 
 let rec gcd_aux p m n: nat \def
 match divides_b n m with
diff --git a/matita/library_auto/nat/le_arith.ma b/matita/library_auto/auto/nat/le_arith.ma
similarity index 98%
rename from matita/library_auto/nat/le_arith.ma
rename to matita/library_auto/auto/nat/le_arith.ma
index 55a9c7e82..ea50a2476 100644
--- a/matita/library_auto/nat/le_arith.ma
+++ b/matita/library_auto/auto/nat/le_arith.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/le_arith".
 
-include "nat/times.ma".
-include "nat/orders.ma".
+include "auto/nat/times.ma".
+include "auto/nat/orders.ma".
 
 (* plus *)
 theorem monotonic_le_plus_r: 
diff --git a/matita/library_auto/nat/lt_arith.ma b/matita/library_auto/auto/nat/lt_arith.ma
similarity index 99%
rename from matita/library_auto/nat/lt_arith.ma
rename to matita/library_auto/auto/nat/lt_arith.ma
index dabfcf835..4c0578623 100644
--- a/matita/library_auto/nat/lt_arith.ma
+++ b/matita/library_auto/auto/nat/lt_arith.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/lt_arith".
 
-include "nat/div_and_mod.ma".
+include "auto/nat/div_and_mod.ma".
 
 (* plus *)
 theorem monotonic_lt_plus_r: 
diff --git a/matita/library_auto/nat/map_iter_p.ma b/matita/library_auto/auto/nat/map_iter_p.ma
similarity index 99%
rename from matita/library_auto/nat/map_iter_p.ma
rename to matita/library_auto/auto/nat/map_iter_p.ma
index d686d9f89..7ac81c367 100644
--- a/matita/library_auto/nat/map_iter_p.ma
+++ b/matita/library_auto/auto/nat/map_iter_p.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/map_iter_p.ma".
 
-include "nat/permutation.ma".
-include "nat/count.ma".
+include "auto/nat/permutation.ma".
+include "auto/nat/count.ma".
 
 let rec map_iter_p n p (g:nat \to nat) (a:nat) f \def
   match n with
diff --git a/matita/library_auto/nat/minimization.ma b/matita/library_auto/auto/nat/minimization.ma
similarity index 99%
rename from matita/library_auto/nat/minimization.ma
rename to matita/library_auto/auto/nat/minimization.ma
index c940e4e6c..84d6b4181 100644
--- a/matita/library_auto/nat/minimization.ma
+++ b/matita/library_auto/auto/nat/minimization.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/minimization".
 
-include "nat/minus.ma".
+include "auto/nat/minus.ma".
 
 let rec max i f \def
   match (f i) with 
diff --git a/matita/library_auto/nat/minus.ma b/matita/library_auto/auto/nat/minus.ma
similarity index 99%
rename from matita/library_auto/nat/minus.ma
rename to matita/library_auto/auto/nat/minus.ma
index 3fbf92a29..e7b01f9da 100644
--- a/matita/library_auto/nat/minus.ma
+++ b/matita/library_auto/auto/nat/minus.ma
@@ -15,8 +15,8 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/minus".
 
-include "nat/le_arith.ma".
-include "nat/compare.ma".
+include "auto/nat/le_arith.ma".
+include "auto/nat/compare.ma".
 
 let rec minus n m \def 
  match n with 
diff --git a/matita/library_auto/nat/nat.ma b/matita/library_auto/auto/nat/nat.ma
similarity index 100%
rename from matita/library_auto/nat/nat.ma
rename to matita/library_auto/auto/nat/nat.ma
diff --git a/matita/library_auto/nat/nth_prime.ma b/matita/library_auto/auto/nat/nth_prime.ma
similarity index 99%
rename from matita/library_auto/nat/nth_prime.ma
rename to matita/library_auto/auto/nat/nth_prime.ma
index 91e66f741..edc677b2f 100644
--- a/matita/library_auto/nat/nth_prime.ma
+++ b/matita/library_auto/auto/nat/nth_prime.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/nth_prime".
 
-include "nat/primes.ma".
-include "nat/lt_arith.ma".
+include "auto/nat/primes.ma".
+include "auto/nat/lt_arith.ma".
 
 (* upper bound by Bertrand's conjecture. *)
 (* Too difficult to prove.        
diff --git a/matita/library_auto/nat/ord.ma b/matita/library_auto/auto/nat/ord.ma
similarity index 98%
rename from matita/library_auto/nat/ord.ma
rename to matita/library_auto/auto/nat/ord.ma
index 3527ac45a..3df876c69 100644
--- a/matita/library_auto/nat/ord.ma
+++ b/matita/library_auto/auto/nat/ord.ma
@@ -15,9 +15,9 @@
 set "baseuri" "cic:/matita/library_auto/nat/ord".
 
 include "datatypes/constructors.ma".
-include "nat/exp.ma".
-include "nat/gcd.ma".
-include "nat/relevant_equations.ma". (* required by auto paramod *)
+include "auto/nat/exp.ma".
+include "auto/nat/gcd.ma".
+include "auto/nat/relevant_equations.ma". (* required by auto paramod *)
 
 (* this definition of log is based on pairs, with a remainder *)
 
@@ -385,4 +385,4 @@ apply p_ord_exp1
   (*rewrite < times_n_SO.
   apply exp_n_SO*)
 ]
-qed.
\ No newline at end of file
+qed.
diff --git a/matita/library_auto/nat/orders.ma b/matita/library_auto/auto/nat/orders.ma
similarity index 99%
rename from matita/library_auto/nat/orders.ma
rename to matita/library_auto/auto/nat/orders.ma
index 5dcfa6471..0ae30794c 100644
--- a/matita/library_auto/nat/orders.ma
+++ b/matita/library_auto/auto/nat/orders.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/orders".
 
-include "nat/nat.ma".
+include "auto/nat/nat.ma".
 include "higher_order_defs/ordering.ma".
 
 (* definitions *)
diff --git a/matita/library_auto/nat/permutation.ma b/matita/library_auto/auto/nat/permutation.ma
similarity index 99%
rename from matita/library_auto/nat/permutation.ma
rename to matita/library_auto/auto/nat/permutation.ma
index b560d9408..b3b9dae8d 100644
--- a/matita/library_auto/nat/permutation.ma
+++ b/matita/library_auto/auto/nat/permutation.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/permutation".
 
-include "nat/compare.ma".
-include "nat/sigma_and_pi.ma".
+include "auto/nat/compare.ma".
+include "auto/nat/sigma_and_pi.ma".
 
 definition injn: (nat \to nat) \to nat \to Prop \def
 \lambda f:nat \to nat.\lambda n:nat.\forall i,j:nat. 
diff --git a/matita/library_auto/nat/plus.ma b/matita/library_auto/auto/nat/plus.ma
similarity index 98%
rename from matita/library_auto/nat/plus.ma
rename to matita/library_auto/auto/nat/plus.ma
index 4855b23ce..02b819f46 100644
--- a/matita/library_auto/nat/plus.ma
+++ b/matita/library_auto/auto/nat/plus.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/plus".
 
-include "nat/nat.ma".
+include "auto/nat/nat.ma".
 
 let rec plus n m \def 
  match n with 
diff --git a/matita/library_auto/nat/primes.ma b/matita/library_auto/auto/nat/primes.ma
similarity index 99%
rename from matita/library_auto/nat/primes.ma
rename to matita/library_auto/auto/nat/primes.ma
index af6d9245b..dc19fb65b 100644
--- a/matita/library_auto/nat/primes.ma
+++ b/matita/library_auto/auto/nat/primes.ma
@@ -14,10 +14,10 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/primes".
 
-include "nat/div_and_mod.ma".
-include "nat/minimization.ma".
-include "nat/sigma_and_pi.ma".
-include "nat/factorial.ma".
+include "auto/nat/div_and_mod.ma".
+include "auto/nat/minimization.ma".
+include "auto/nat/sigma_and_pi.ma".
+include "auto/nat/factorial.ma".
 
 inductive divides (n,m:nat) : Prop \def
 witness : \forall p:nat.m = times n p \to divides n m.
diff --git a/matita/library_auto/nat/relevant_equations.ma b/matita/library_auto/auto/nat/relevant_equations.ma
similarity index 95%
rename from matita/library_auto/nat/relevant_equations.ma
rename to matita/library_auto/auto/nat/relevant_equations.ma
index f905d2120..e057351b3 100644
--- a/matita/library_auto/nat/relevant_equations.ma
+++ b/matita/library_auto/auto/nat/relevant_equations.ma
@@ -14,9 +14,9 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/relevant_equations".
 
-include "nat/times.ma".
-include "nat/minus.ma".
-include "nat/gcd.ma". 
+include "auto/nat/times.ma".
+include "auto/nat/minus.ma".
+include "auto/nat/gcd.ma". 
 (* if gcd is compiled before this, the applys will take too much *)
 
 theorem times_plus_l: \forall n,m,p:nat. (n+m)*p = n*p + m*p.
diff --git a/matita/library_auto/nat/sigma_and_pi.ma b/matita/library_auto/auto/nat/sigma_and_pi.ma
similarity index 97%
rename from matita/library_auto/nat/sigma_and_pi.ma
rename to matita/library_auto/auto/nat/sigma_and_pi.ma
index 983e7644f..c571b48e4 100644
--- a/matita/library_auto/nat/sigma_and_pi.ma
+++ b/matita/library_auto/auto/nat/sigma_and_pi.ma
@@ -14,9 +14,9 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/sigma_and_pi".
 
-include "nat/factorial.ma".
-include "nat/exp.ma".
-include "nat/lt_arith.ma".
+include "auto/nat/factorial.ma".
+include "auto/nat/exp.ma".
+include "auto/nat/lt_arith.ma".
 
 let rec sigma n f m \def
   match n with 
diff --git a/matita/library_auto/nat/times.ma b/matita/library_auto/auto/nat/times.ma
similarity index 99%
rename from matita/library_auto/nat/times.ma
rename to matita/library_auto/auto/nat/times.ma
index 60ebc0347..89cfd4b82 100644
--- a/matita/library_auto/nat/times.ma
+++ b/matita/library_auto/auto/nat/times.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/times".
 
-include "nat/plus.ma".
+include "auto/nat/plus.ma".
 
 let rec times n m \def 
  match n with 
diff --git a/matita/library_auto/nat/totient.ma b/matita/library_auto/auto/nat/totient.ma
similarity index 98%
rename from matita/library_auto/nat/totient.ma
rename to matita/library_auto/auto/nat/totient.ma
index f95399a30..c4e1d5ad9 100644
--- a/matita/library_auto/nat/totient.ma
+++ b/matita/library_auto/auto/nat/totient.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/library_auto/nat/totient".
 
-include "nat/count.ma".
-include "nat/chinese_reminder.ma".
+include "auto/nat/count.ma".
+include "auto/nat/chinese_reminder.ma".
 
 definition totient : nat \to nat \def
 \lambda n. count n (\lambda m. eqb (gcd m n) (S O)).
diff --git a/matita/library_auto/makefile b/matita/library_auto/makefile
new file mode 100644
index 000000000..c4020f673
--- /dev/null
+++ b/matita/library_auto/makefile
@@ -0,0 +1,39 @@
+H=@
+
+RT_BASEDIR=../
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) 
+
+devel:=$(shell basename `pwd`)
+
+ifneq "$(SRC)" ""
+  XXX="SRC=$(SRC)"
+endif
+
+all: preall
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall.opt
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall.opt
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall.opt
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall.opt
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+	
+preall:
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+
+preall.opt:
+	$(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel)
-- 
2.39.2