Committing all the recent development of Andrea after the merge between his

[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 e725185e004bfaedb6ed3dbbea63720bd91ab4ba..1b790031401c2aeb8dc04a3ad769fd9f43fa86c6 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -15,7 +15,7 @@
 
 set "baseuri" "cic:/matita/nat/minus".
 
-include "nat/orders_op.ma".
+include "nat/le_arith.ma".
 include "nat/compare.ma".
 
 let rec minus n m \def 
@@ -98,6 +98,20 @@ symmetry.
 apply plus_minus_m_m.assumption.
 qed.
 
+theorem minus_S_S : \forall n,m:nat.
+eq nat (minus (S n) (S m)) (minus n m).
+intros.
+reflexivity.
+qed.
+
+theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to 
+eq nat (minus (pred n) (pred m)) (minus n m).
+intros.
+apply lt_O_n_elim n H.intro.
+apply lt_O_n_elim m H1.intro.
+simplify.reflexivity.
+qed.
+
 theorem eq_minus_n_m_O: \forall n,m:nat.
 n \leq m \to n-m = O.
 intros 2.