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

[helm.git] / helm / matita / library / nat / compare.ma

diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index 22c8b25a790d1551df8d23d55847352e9eb9f9b6..e20d824df5ae105129599fda2b93beac3a23fcfb 100644 (file)
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -89,7 +89,7 @@ simplify.intros.apply H.apply le_S_S_to_le.assumption.
 qed.
 
 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
-(n \leq m \to (P true)) \to (\not (n \leq m) \to (P false)) \to
+(n \leq m \to (P true)) \to (\lnot (n \leq m) \to (P false)) \to
 P (leb n m).
 intros.
 cut