New version of the library. nth_prime, gcd, log.

[helm.git] / helm / matita / library / nat / minus.ma

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 7945a76e01c3c36ebe2d68ad3eda850af1bf4186..6ff744dcb5a3aa5e8cc626b20ae2740bda00b49c 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -153,6 +153,12 @@ intros.simplify.apply le_n.
 intros.simplify.apply le_S.assumption.
 qed.
 
+theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
+intros.apply lt_O_n_elim n H.intro.
+apply lt_O_n_elim m H1.intro.
+simplify.apply le_S_S.apply le_minus_m.
+qed.
+
 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
 intros 2.
 apply nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m).
@@ -232,3 +238,41 @@ qed.
 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 \def distributive_times_minus.
 
+theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
+intros.
+cut m+p \le n \or \not m+p \le n.
+elim Hcut.
+apply sym_eq.
+apply plus_to_minus.assumption.
+rewrite > assoc_plus.
+rewrite > sym_plus p.
+rewrite < plus_minus_m_m.
+rewrite > sym_plus.
+rewrite < plus_minus_m_m.reflexivity.
+rewrite > eq_minus_n_m_O n (m+p).
+rewrite > eq_minus_n_m_O (n-m) p.reflexivity.
+apply decidable_le (m+p) n.
+apply le_plus_to_minus_r.
+rewrite > sym_plus.assumption.
+apply trans_le ? (m+p).
+rewrite < sym_plus.
+apply le_plus_n.assumption.
+apply lt_to_le.apply not_le_to_lt.assumption.
+apply le_plus_to_minus.
+apply lt_to_le.apply not_le_to_lt.
+rewrite < sym_plus.assumption.
+qed.
+
+theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
+p+(n-m) = n-(m-p).
+intros.
+apply sym_eq.
+apply plus_to_minus.
+apply le_plus_to_minus.
+apply trans_le ? n.assumption.rewrite < sym_plus.apply le_plus_n.
+rewrite < assoc_plus.
+rewrite < plus_minus_m_m.
+rewrite < sym_plus.
+rewrite < plus_minus_m_m.reflexivity.
+assumption.assumption.
+qed.