From 5a702cea95883f7095c16b450e065ccb1714fc5a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 Sep 2005 09:20:00 +0000
Subject: [PATCH] .ma inclusions corrected/minimized

---
 helm/matita/library/Q/q.ma                         |  1 -
 helm/matita/library/Z/compare.ma                   |  2 --
 helm/matita/library/Z/plus.ma                      |  1 -
 helm/matita/library/Z/times.ma                     |  1 -
 helm/matita/library/Z/z.ma                         |  2 +-
 helm/matita/library/higher_order_defs/functions.ma |  1 -
 helm/matita/library/logic/equality.ma              |  1 -
 helm/matita/library/nat/div_and_mod.ma             |  2 --
 helm/matita/library/nat/exp.ma                     | 11 ++++-------
 helm/matita/library/nat/factorial.ma               |  2 +-
 helm/matita/library/nat/gcd.ma                     |  1 -
 helm/matita/library/nat/le_arith.ma                |  2 --
 helm/matita/library/nat/log.ma                     |  3 ++-
 helm/matita/library/nat/lt_arith.ma                |  1 -
 helm/matita/library/nat/nat.ma                     |  3 ---
 helm/matita/library/nat/nth_prime.ma               |  1 +
 helm/matita/library/nat/orders.ma                  |  2 +-
 helm/matita/library/nat/primes1.ma                 |  1 -
 helm/matita/library/nat/sigma_and_pi.ma            |  5 +----
 19 files changed, 11 insertions(+), 32 deletions(-)

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index d7c2816a1..4878078fc 100644
--- a/helm/matita/library/Q/q.ma
+++ b/helm/matita/library/Q/q.ma
@@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/Q/q".
 
 include "Z/compare.ma".
 include "Z/plus.ma".
-include "higher_order_defs/functions.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/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma
index a8f8aca39..3b259b4f6 100644
--- a/helm/matita/library/Z/compare.ma
+++ b/helm/matita/library/Z/compare.ma
@@ -14,8 +14,6 @@
 
 set "baseuri" "cic:/matita/Z/compare".
 
-include "datatypes/bool.ma".
-include "datatypes/compare.ma".
 include "Z/orders.ma".
 include "nat/compare.ma".
 
diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma
index 56b960403..dc743e60b 100644
--- a/helm/matita/library/Z/plus.ma
+++ b/helm/matita/library/Z/plus.ma
@@ -15,7 +15,6 @@
 set "baseuri" "cic:/matita/Z/plus".
 
 include "Z/z.ma".
-include "nat/compare.ma".
 include "nat/minus.ma".
 
 definition Zplus :Z \to Z \to Z \def
diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 72e8177b8..c4e965fbf 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/Z/times".
 
 include "nat/lt_arith.ma".
 include "Z/plus.ma".
-include "higher_order_defs/functions.ma".
 
 definition Ztimes :Z \to Z \to Z \def
 \lambda x,y.
diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index 207457a91..997229763 100644
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/Z/z".
 
+include "datatypes/bool.ma".
 include "nat/nat.ma".
-include "higher_order_defs/functions.ma".
 
 inductive Z : Set \def
   OZ : Z
diff --git a/helm/matita/library/higher_order_defs/functions.ma b/helm/matita/library/higher_order_defs/functions.ma
index 71b6d8459..da90d4211 100644
--- a/helm/matita/library/higher_order_defs/functions.ma
+++ b/helm/matita/library/higher_order_defs/functions.ma
@@ -15,7 +15,6 @@
 set "baseuri" "cic:/matita/higher_order_defs/functions/".
 
 include "logic/equality.ma".
-include "logic/connectives.ma".
 
 definition injective: \forall A,B:Type.\forall f:A \to B.Prop
 \def \lambda A,B.\lambda f.
diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 84f7df2e6..a5d2f0d1e 100644
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -15,7 +15,6 @@
 set "baseuri" "cic:/matita/logic/equality/".
 
 include "higher_order_defs/relations.ma".
-include "logic/connectives.ma".
 
 inductive eq (A:Type) (x:A) : A \to Prop \def
     refl_eq : eq A x x.
diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index 73f90e553..ede15596a 100644
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -15,8 +15,6 @@
 set "baseuri" "cic:/matita/nat/div_and_mod".
 
 include "nat/minus.ma".
-include "nat/le_arith.ma".
-include "nat/compare.ma".
 
 let rec mod_aux p m n: nat \def
 match (leb m n) with
diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma
index 2f0bfbeaf..a80a0cee3 100644
--- a/helm/matita/library/nat/exp.ma
+++ b/helm/matita/library/nat/exp.ma
@@ -14,9 +14,7 @@
 
 set "baseuri" "cic:/matita/nat/exp".
 
-include "nat/times.ma". 
-include "nat/orders.ma".
-include "higher_order_defs/functions.ma".
+include "nat/div_and_mod.ma".
 
 let rec exp n m on m\def 
  match m with 
@@ -88,11 +86,10 @@ assumption.
 intros 2.
 apply nat_case n.
 intros.apply False_ind.apply not_le_Sn_O O H3.
-intros.apply inj_times_r m1.assumption.
+intros.
+apply inj_times_r m1.assumption.
 qed.
 
 variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
 (exp p n) = (exp p m) \to n = m \def
-injective_exp_r.
-
-
+injective_exp_r.
\ No newline at end of file
diff --git a/helm/matita/library/nat/factorial.ma b/helm/matita/library/nat/factorial.ma
index 742ca2a3b..50345ee12 100644
--- a/helm/matita/library/nat/factorial.ma
+++ b/helm/matita/library/nat/factorial.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/nat/factorial".
 
-include "nat/lt_arith.ma".
+include "nat/le_arith.ma".
 
 let rec fact n \def
   match n with 
diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index 921d8853e..587314315 100644
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -15,7 +15,6 @@
 set "baseuri" "cic:/matita/nat/gcd".
 
 include "nat/primes.ma".
-include "higher_order_defs/functions.ma".
 
 let rec gcd_aux p m n: nat \def
 match divides_b n m with
diff --git a/helm/matita/library/nat/le_arith.ma b/helm/matita/library/nat/le_arith.ma
index a36f96bd4..dbf7b1c42 100644
--- a/helm/matita/library/nat/le_arith.ma
+++ b/helm/matita/library/nat/le_arith.ma
@@ -14,10 +14,8 @@
 
 set "baseuri" "cic:/matita/nat/le_arith".
 
-include "higher_order_defs/functions.ma".
 include "nat/times.ma".
 include "nat/orders.ma".
-include "nat/compare.ma".
 
 (* plus *)
 theorem monotonic_le_plus_r: 
diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index e24c3031f..301c0be8e 100644
--- a/helm/matita/library/nat/log.ma
+++ b/helm/matita/library/nat/log.ma
@@ -15,8 +15,9 @@
 set "baseuri" "cic:/matita/nat/log".
 
 include "datatypes/constructors.ma".
-include "nat/primes.ma".
 include "nat/exp.ma".
+include "nat/lt_arith.ma".
+include "nat/primes.ma".
 
 (* this definition of log is based on pairs, with a remainder *)
 
diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index 85280fe0f..dd4fdcbf9 100644
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -14,7 +14,6 @@
 
 set "baseuri" "cic:/matita/nat/lt_arith".
 
-include "nat/exp.ma".
 include "nat/div_and_mod.ma".
 
 (* plus *)
diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index f8ff252ae..100cb0f03 100644
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -14,9 +14,6 @@
 
 set "baseuri" "cic:/matita/nat/nat".
 
-include "datatypes/bool.ma".
-include "logic/equality.ma".
-include "logic/connectives.ma".
 include "higher_order_defs/functions.ma".
 
 inductive nat : Set \def
diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index ee21195dc..37c60b405 100644
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -15,6 +15,7 @@
 set "baseuri" "cic:/matita/nat/nth_prime".
 
 include "nat/primes.ma".
+include "nat/lt_arith.ma".
 
 (* upper bound by Bertrand's conjecture. *)
 (* Too difficult to prove.        
diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 811706867..a162df9a3 100644
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/nat/orders".
 
-include "nat/plus.ma".
+include "nat/nat.ma".
 include "higher_order_defs/ordering.ma".
 
 (* definitions *)
diff --git a/helm/matita/library/nat/primes1.ma b/helm/matita/library/nat/primes1.ma
index 55d643262..3df3922a4 100644
--- a/helm/matita/library/nat/primes1.ma
+++ b/helm/matita/library/nat/primes1.ma
@@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/nat/primes1".
 
 include "datatypes/constructors.ma".
 include "nat/primes.ma".
-include "nat/exp.ma".
 
 (* p is just an upper bound, acc is an accumulator *)
 let rec n_divides_aux p n m acc \def
diff --git a/helm/matita/library/nat/sigma_and_pi.ma b/helm/matita/library/nat/sigma_and_pi.ma
index b9b8065aa..29df3a1df 100644
--- a/helm/matita/library/nat/sigma_and_pi.ma
+++ b/helm/matita/library/nat/sigma_and_pi.ma
@@ -24,7 +24,4 @@ let rec sigma n f \def
 let rec pi n f \def
   match n with 
   [ O \Rightarrow (S O)
-  | (S p) \Rightarrow (f p)*(pi p f)].
-
-
-
+  | (S p) \Rightarrow (f p)*(pi p f)].
\ No newline at end of file
-- 
2.39.2