Several changes. Proof of Fermat's little theorem completed.

[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 8302f7ce5873aee8dc6f7893065068e0fb38feb7..0c8780f7e68a50e0b453a5fe2dff09707704c214 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -68,6 +68,18 @@ intros.simplify.reflexivity.
 intros.simplify.apply H.apply le_S_S_to_le.assumption.
 qed.
 
+theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
+intros 2.
+generalize in match n.
+elim m.
+rewrite < minus_n_O.apply plus_n_O.
+elim n2.simplify.
+apply minus_n_n.
+rewrite < plus_n_Sm.
+change with S n3 = (S n3 + n1)-n1.
+apply H.
+qed.
+
 theorem plus_minus_m_m: \forall n,m:nat.
 m \leq n \to n = (n-m)+m.
 intros 2.