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

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 06266a4b0..5b430d7c6 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -305,6 +305,10 @@ lemma lt_to_le: ∀x,y. x < y → x ≤ y.
 lemma inv_eq_minus_O: ∀x,y. x - y = 0 → x ≤ y.
 // qed-.
 
+lemma le_x_times_x: ∀x. x ≤ x * x.
+#x elim x -x //
+qed.
+
 (* lt *)
 
 theorem transitive_lt: transitive nat lt.
@@ -491,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.
@@ -645,6 +661,14 @@ theorem monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
 @lt_plus_to_minus_r <plus_minus_m_m //
 qed.
 
+(* More compound conclusion *************************************************)
+
+lemma discr_minus_x_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
+* /2 width=1/ #x * /2 width=1/ #y normalize #H 
+lapply (minus_le x y) <H -H #H
+elim (not_le_Sn_n x) #H0 elim (H0 ?) //
+qed-.
+
 (* Still more equalities ****************************************************)
 
 theorem eq_minus_O: ∀n,m:nat.
@@ -688,11 +712,8 @@ qed.
 lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
 /2 width=1/ qed.
 
-lemma discr_minus_x_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
-* /2 width=1/ #x * /2 width=1/ #y normalize #H 
-lapply (minus_le x y) <H -H #H
-elim (not_le_Sn_n x) #H0 elim (H0 ?) //
-qed-.
+lemma minus_plus_plus_l: ∀x,y,h. (x + h) - (y + h) = x - y.
+// qed.
 
 (* Stilll more atomic conclusion ********************************************)