X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat.txt;h=915a45dbfa2363190f3d6e466aceba866c53be19;hb=68e028d053806177e218ee1a5f8778d3011bef83;hp=fc8e9e241fdf0538f9560c1336f1a93ebb497f42;hpb=5e72e41f4f86814e56d4b00959ccc56c71042a4c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
index fc8e9e241..915a45dbf 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
@@ -111,23 +111,24 @@
 #
 "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"
+#
+"cic:/matita/arithmetics/nat/max.con"
+"cic:/matita/arithmetics/nat/commutative_max.con"
 
 ####################################
 
 "cic:/matita/arithmetics/nat/to_max.con"
-"cic:/matita/arithmetics/nat/commutative_max.con"
 "cic:/matita/arithmetics/nat/leb.con"
 "cic:/matita/arithmetics/nat/leb_elim.con"
 "cic:/matita/arithmetics/nat/le_maxl.con"
 "cic:/matita/arithmetics/nat/le_maxr.con"
 "cic:/matita/arithmetics/nat/le_to_leb_true.con"
-"cic:/matita/arithmetics/nat/max.con"
 "cic:/matita/arithmetics/nat/not_le_to_leb_false.con"
 
 "cic:/matita/arithmetics/nat/nat_discr.con"