]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/arith/nat.txt
arithmetics for λδ
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat.txt
index fc8e9e241fdf0538f9560c1336f1a93ebb497f42..2bd0eabca2a0c38253dfe23fe7501864a7665e33 100644 (file)
 #
 "cic:/matita/arithmetics/nat/minus_pred_pred.con"
 "cic:/matita/arithmetics/nat/monotonic_lt_minus_l.con"
-
-"cic:/matita/arithmetics/nat/lt_minus_to_plus.con"
-"cic:/matita/arithmetics/nat/lt_minus_to_plus_r.con"
+#
 "cic:/matita/arithmetics/nat/lt_plus_to_minus.con"
 "cic:/matita/arithmetics/nat/lt_plus_to_minus_r.con"
 "cic:/matita/arithmetics/nat/lt_inv_plus_l.con"
+"cic:/matita/arithmetics/nat/lt_minus_to_plus.con"
+"cic:/matita/arithmetics/nat/lt_minus_to_plus_r.con"
 
 ####################################