addition for natural numbers with infinity

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / ynat / ynat_succ.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
index c244b9caed637c9567846f7515f054511f3a57f4..a8d1946bea235170f6405cdcc962f660c1e789ae 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
@@ -38,6 +38,11 @@ lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m. n = ⫯m.
 ]
 qed-.
 
+lemma ysucc_iter_Y: ∀m. ysucc^m (∞) = ∞.
+#m elim m -m //
+#m #IHm whd in ⊢ (??%?); >IHm //
+qed.
+
 (* Inversion lemmas *********************************************************)
 
 lemma ysucc_inj: ∀m,n. ⫯m = ⫯n → m = n.