.ma inclusions corrected/minimized

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index d7c2816a15cbdc8997d27d5472b82e0fe5be66cf..4878078fc44482f8ed80b3d138c27d7ba9446726 100644 (file)
--- 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 a8f8aca3918f12c1a7a60fb475338a81da32dfbe..3b259b4f664b0b19d1d8ec646596600e135e693e 100644 (file)
--- 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 56b960403b7f00e2a9e3e5b4158742a9288ec179..dc743e60bc77f384ecdadd927cee18d5ae085461 100644 (file)
--- 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 72e8177b8a559e26be039f624bf1797f0c04fc3c..c4e965fbf356f7e198a8e24f7d26d3767ad70700 100644 (file)
--- 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 207457a913e4e9c91574cf2e630ea61f3f2feb93..997229763f5fc77f4a62790ffe009bd1d65cd0f0 100644 (file)
--- 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 71b6d84599df20cfcd223a7565e4c83bb85f03e5..da90d421177817ff8561794d66250f97c6ce4fda 100644 (file)
--- 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 84f7df2e66144c8a90a74a757af063c9b674709f..a5d2f0d1e461cd5c02e95aa5f2eb1ec04f96d5fd 100644 (file)
--- 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 73f90e55371c3440aad9bd8e51a116f4bd1b7b7c..ede15596aad479399b646b5f3e78ad9b423cc2fb 100644 (file)
--- 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 2f0bfbeaf50b8166fd3f95c9cb6b9c83551dd723..a80a0cee362fc3fd4024dd565faec8df6d6f4373 100644 (file)
--- 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 742ca2a3ba517b2b0d7942076a8ee70edb0a35d5..50345ee121e62aca628e4e82b9811e040199d08b 100644 (file)
--- 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 921d8853e87a6cf03fee66f79bdfb4f6a1e0bfc2..587314315268fc875ab715ab21ac83fd694c1613 100644 (file)
--- 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 a36f96bd451caba6a4091f0e7ecd9ea530957ed1..dbf7b1c4298ca340b14791da95e44f1bfab3e988 100644 (file)
--- 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 e24c3031f7873767920d1c6934be5cc65981f715..301c0be8ef1dc689646af66e4321177c2cb5372f 100644 (file)
--- 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 85280fe0f2da8aef41e9e030c42428b82d30f7ea..dd4fdcbf98a1e6e5c0667907c4c080c52b0c5696 100644 (file)
--- 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 f8ff252aeae6c4e11ae88c484eac2908fd507d33..100cb0f0356afccc78a3b06f8c2c7e62da4953a0 100644 (file)
--- 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 ee21195dc10bd823f4a96b8998a87ad99f6bb562..37c60b4057713ac77ddf68e638b2279db7f235a9 100644 (file)
--- 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 811706867e4729f52f57ffd1d7f9183073c122f2..a162df9a3c418a6ca0761b64bbf44da513bda072 100644 (file)
--- 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 55d643262e15b4d4201359a0a6f0c01d515c9871..3df3922a4887d50e19fc4ec3e0f5acfffadb2ec4 100644 (file)
--- 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 b9b8065aa6732ea934d5fcdac6289557d9852a29..29df3a1dfdab2b76f726748897621bd7758dd3d1 100644 (file)
--- 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