X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=5b430d7c651fd8521feedf30f8cf8531f0e3677e;hb=77bf99a9ac05a61573d621d576e269870668f076;hp=56935028f65015812b79fdc15fb8762b012d14cf;hpb=9def1b8a298aac85a7abdc75c4a33657fe7e6df7;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 56935028f..5b430d7c6 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -495,6 +495,18 @@ cut (∀q:nat. q ≤ n → P q) /2/
  ]
 qed.
 
+fact f_ind_aux: ∀A. ∀f:A→ℕ. ∀P:predicate A.
+                (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) →
+                ∀n,a. f a = n → P a.
+#A #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
+qed-.
+
+lemma f_ind: ∀A. ∀f:A→ℕ. ∀P:predicate A.
+             (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) → ∀a. P a.
+#A #f #P #H #a
+@(f_ind_aux … H) -H [2: // | skip ]
+qed-. 
+
 (* More negated equalities **************************************************)
 
 theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.