More notation here and there.

[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 cbf92049cc852bb02535156554a30f0e83906378..3b39ed43f1faa363340d95fbfe24ef191c98f15d 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -235,7 +235,7 @@ theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 
 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
 intros.
-cut m+p \le n \or \lnot m+p \le n.
+cut m+p \le n \or m+p \nleq n.
   elim Hcut.
     symmetry.apply plus_to_minus.assumption.
     rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.