X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=e80380217218b13d13dc41a247c8bf503cb4bff8;hb=e8998d29ab83e7b6aa495a079193705b2f6743d3;hp=5b430d7c651fd8521feedf30f8cf8531f0e3677e;hpb=bde429ac54e48de74b3d8b1df72dfcb86aa9bae5;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 5b430d7c6..e80380217 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -505,6 +505,19 @@ 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-.
+
+fact f2_ind_aux: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2.
+                 (∀n. (∀a1,a2. f a1 a2 < n → P a1 a2) → ∀a1,a2. f a1 a2 = n → P a1 a2) →
+                 ∀n,a1,a2. f a1 a2 = n → P a1 a2.
+#A1 #A2 #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
+qed-.
+
+lemma f2_ind: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2.
+              (∀n. (∀a1,a2. f a1 a2 < n → P a1 a2) → ∀a1,a2. f a1 a2 = n → P a1 a2) →
+              ∀a1,a2. P a1 a2.
+#A1 #A2 #f #P #H #a1 #a2
+@(f2_ind_aux … H) -H [2: // | skip ]
 qed-. 
 
 (* More negated equalities **************************************************)