Totient function and related files.

[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 4910f3003541fb0a94f99b1072012ee0ea21d6d0..1ee70bd39c0a19088ebc2fb1d12dfbdf28add444 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -225,6 +225,16 @@ apply H.apply le_S_S_to_le.
 rewrite > plus_n_Sm.assumption.
 qed.
 
+(* minus and lt - to be completed *)
+theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
+intros 3.apply nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p)).
+intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
+simplify.intros.apply False_ind.apply not_le_Sn_O n H.
+simplify.intros.
+apply le_S_S.
+rewrite < plus_n_Sm.
+apply H.apply H1.
+qed.
 
 theorem distributive_times_minus: distributive nat times minus.
 simplify.
@@ -247,6 +257,15 @@ qed.
 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 \def distributive_times_minus.
 
+theorem eq_minus_plus_plus_minus: \forall n,m,p:nat. p \le m \to (n+m)-p = n+(m-p).
+intros.
+apply plus_to_minus.
+rewrite > sym_plus in \vdash (? ? ? %).
+rewrite > assoc_plus.
+rewrite < plus_minus_m_m.
+reflexivity.assumption.
+qed.
+
 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
 intros.
 cut (m+p \le n \or m+p \nleq n).