X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fiteration.ma;h=407e12b032429c0a430d8104f37768688fca446f;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=78d4eb4d01f67a852cd1544ced197c5bb91d7105;hpb=68b4f2490c12139c03760b39895619e63b0f38c9;p=helm.git

diff --git a/matita/matita/lib/arithmetics/iteration.ma b/matita/matita/lib/arithmetics/iteration.ma
index 78d4eb4d0..407e12b03 100644
--- a/matita/matita/lib/arithmetics/iteration.ma
+++ b/matita/matita/lib/arithmetics/iteration.ma
@@ -10,6 +10,7 @@
       V_______________________________________________________________ *)
 
 include "arithmetics/nat.ma".
+include "basics/core_notation/exp_2.ma".
 
 (* iteration *) 
 
@@ -43,4 +44,4 @@ lemma monotonic_iter2: ∀g,a,i,j. (∀x. x ≤ g x) → i ≤ j →
   g^i a ≤  g^j a.
 #g #a #i #j #leg #leij elim leij //
 #m #leim #Hind normalize @(transitive_le … Hind) @leg 
-qed.
\ No newline at end of file
+qed.