.ma inclusions corrected/minimized

[helm.git] / helm / matita / library / nat / exp.ma

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