Removed duplicated notation and interaction with the user.

[helm.git] / matita / matita / lib / arithmetics / nat.ma

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 31d5ced7f7c64ac7dfa03ee8b6f96c65ad12a09b..81d6c9310247dc42c5f2d0d76e66a986ae1d45fc 100644 (file)
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -450,8 +450,16 @@ lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
 #m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/
 qed-.
 
+lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
+#m #n elim (decidable_le m n) /2 width=1/ /4 width=2/
+qed-.
+
 (* More general conclusion **************************************************)
 
+theorem nat_ind_plus: ∀R:predicate nat.
+                      R 0 → (∀n. R n → R (n + 1)) → ∀n. R n.
+/3 width=1 by nat_ind/ qed-.
+
 theorem lt_O_n_elim: ∀n:nat. 0 < n → 
   ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
 #n (elim n) // #abs @False_ind /2/ @absurd
@@ -666,6 +674,9 @@ lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
 #b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); //
 qed.
 
+lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
+/2 width=1/ qed.
+
 (* Stilll more atomic conclusion ********************************************)
 
 (* le *)