Notation for equality used everywhere.

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

diff --git a/helm/matita/library/nat/orders_op.ma b/helm/matita/library/nat/orders_op.ma
index 32a58115dab3dececccbc1eb98fcf9ea431f1ad4..fbfad715c82a6cc155b0cfe24a131a153c58be7d 100644 (file)
--- a/helm/matita/library/nat/orders_op.ma
+++ b/helm/matita/library/nat/orders_op.ma
@@ -52,7 +52,7 @@ intros.change with le (plus O m) (plus n m).
 apply le_plus_l.apply le_O_n.
 qed.
 
-theorem eq_plus_to_le: \forall n,m,p:nat.eq nat n (plus m p) 
+theorem eq_plus_to_le: \forall n,m,p:nat.n=plus m p
 \to le m n.
 intros.rewrite > H.
 rewrite < sym_plus.