update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / arith_2a.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
index b5ff26116ef36e2b41f8e3c4abd9a51fc374f45c..a136174bc8b209fc0c813c013b3382cdca587938 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
@@ -12,16 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/two_0.ma".
+include "ground/arith/pnat_two.ma".
 include "ground/arith/nat_le_minus_plus.ma".
 include "ground/arith/nat_lt.ma".
 
 (* ARITHMETICAL PROPERTIES FOR λδ-2A ****************************************)
 
-interpretation
-  "zero (non-negative integers)"
-  'Two = (ninj (psucc punit)).
-
 (* Equalities ***************************************************************)
 
 lemma plus_n_2: ∀n. (n + 𝟐) = n + 𝟏 + 𝟏.
@@ -87,7 +83,7 @@ lemma lt_plus_SO_to_le: ∀x,y. x < y + (𝟏) → x ≤ y.
 
 (* Iterators ****************************************************************)
 
-lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+𝟏) b = f (f^l b).
+lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. (f^(l+𝟏)) b = f ((f^l) b).
 #B #f #b #l
 <niter_succ //
 qed.