update in standard library

[helm.git] / matita / matita / lib / arithmetics / iteration.ma

diff --git a/matita/matita/lib/arithmetics/iteration.ma b/matita/matita/lib/arithmetics/iteration.ma
index 78d4eb4d01f67a852cd1544ced197c5bb91d7105..407e12b032429c0a430d8104f37768688fca446f 100644 (file)
--- 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.