- subtraction (and related notions) removed

[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 c95c72d152872c8b67f8b063c8be137a911b1c74..c4c989f77d6e2de9869f910d5e67e80682a702ad 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
@@ -88,3 +88,11 @@ qed-.
 
 lemma ysucc_inv_O_dx: ∀m. ⫯m = 0 → ⊥.
 /2 width=2 by ysucc_inv_O_sn/ qed-.
+
+(* Eliminators **************************************************************)
+
+lemma ynat_ind: ∀R:predicate ynat.
+                R 0 → (∀n:nat. R n → R (⫯n)) → R (∞) →
+                ∀x. R x.
+#R #H1 #H2 #H3 * // #n elim n -n /2 width=1 by/
+qed-.