- Level-1: added some problems

[helm.git] / matita / library / legacy / coq.ma

diff --git a/matita/library/legacy/coq.ma b/matita/library/legacy/coq.ma
index 0f5384697ae7d1498f78aaed191080abaad2f46c..092a11c6ae3e7e38c7c6c083e55dc7a5c554ac56 100644 (file)
--- a/matita/library/legacy/coq.ma
+++ b/matita/library/legacy/coq.ma
@@ -81,6 +81,10 @@ interpretation "Coq's natural 'not less or equal than'"
 alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)".
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
+alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
+alias id "le_trans" = "cic:/Coq/Arith/Le/le_trans.con".
+alias id "le_plus_r" = "cic:/Coq/Arith/Plus/le_plus_r.con".
+alias id "le" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)".
 
 (* theorems *)