More notation here and there: \sup, \divides, \ndivides, !

[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 7240b7d09ebbc9f18384e68ae1d51f3dffa8021b..cbf92049cc852bb02535156554a30f0e83906378 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 \not m+p \le n.
+cut m+p \le n \or \lnot m+p \le n.
   elim Hcut.
     symmetry.apply plus_to_minus.assumption.
     rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.