*** empty log message ***

[helm.git] / helm / matita / library / Z / plus.ma

diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma
index dc743e60bc77f384ecdadd927cee18d5ae085461..0456ca0b31533f5aed0ccc9fd7561d67b2b3b2bd 100644 (file)
--- a/helm/matita/library/Z/plus.ma
+++ b/helm/matita/library/Z/plus.ma
@@ -59,12 +59,12 @@ simplify.
 rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
 simplify.
 rewrite > nat_compare_n_m_m_n.
-simplify.elim nat_compare ? ?.simplify.reflexivity.
+simplify.elim nat_compare.simplify.reflexivity.
 simplify. reflexivity.
 simplify. reflexivity.
 elim y.simplify.reflexivity.
 simplify.rewrite > nat_compare_n_m_m_n.
-simplify.elim nat_compare ? ?.simplify.reflexivity.
+simplify.elim nat_compare.simplify.reflexivity.
 simplify. reflexivity.
 simplify. reflexivity.
 simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
@@ -169,10 +169,10 @@ elim H.reflexivity.
 qed.
 
 theorem Zplus_Zsucc_neg_neg : 
-\forall n,m. (Zsucc (neg n))+(neg m) = Zsucc ((neg n)+(neg m)).
+\forall n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
 intros.
 apply nat_elim2
-(\lambda n,m. ((Zsucc (neg n))+(neg m)) = Zsucc ((neg n)+(neg m))).intro.
+(\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)).intro.
 intros.elim n1.
 simplify. reflexivity.
 elim n2.simplify. reflexivity.
@@ -189,7 +189,7 @@ theorem Zplus_Zsucc_neg_pos:
 \forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
 intros.
 apply nat_elim2
-(\lambda n,m. (Zsucc (neg n))+(pos m) = Zsucc ((neg n)+(pos m))).
+(\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m)).
 intros.elim n1.
 simplify. reflexivity.
 elim n2.simplify. reflexivity.