X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flegacy%2Fcoq.ma;h=76da7d8984134a87d4fa1bfea5a440e4b688746d;hb=b74ab91d1db4b1b88471fc47460b6be15a58b162;hp=d3c74fe21e88a02b6ab4e502fcf79c669af0bc19;hpb=37632a908f126ebe1c927cd5c997434d4cd0bf2c;p=helm.git

diff --git a/helm/software/matita/library/legacy/coq.ma b/helm/software/matita/library/legacy/coq.ma
index d3c74fe21..76da7d898 100644
--- a/helm/software/matita/library/legacy/coq.ma
+++ b/helm/software/matita/library/legacy/coq.ma
@@ -56,3 +56,7 @@ interpretation "Coq's real 'greater than'" 'gt x y = (cic:/Coq/Reals/Rdefinition
 interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y).
 interpretation "Coq's not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y)).
 
+interpretation "Coq's natural 'not less or equal than'"
+ 'nleq x y = (cic:/Coq/Init/Logic/not.con 
+               (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y)).
+