arithmetics for λδ

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat.txt

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
index fc8e9e241fdf0538f9560c1336f1a93ebb497f42..72d09cc713713c754e9a4e0ef127b6bdfc5f7c25 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
@@ -111,26 +111,27 @@
 #
 "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/to_max.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/leb.con"
-"cic:/matita/arithmetics/nat/leb_elim.con"
+#
+"cic:/matita/arithmetics/nat/to_max.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"
 "cic:/matita/arithmetics/nat/times.con"
 "cic:/matita/arithmetics/nat/times_n_1.con"
 "cic:/matita/arithmetics/nat/times_Sn_m.con"
+"cic:/matita/arithmetics/nat/leb.con"
+"cic:/matita/arithmetics/nat/leb_elim.con"
+"cic:/matita/arithmetics/nat/le_to_leb_true.con"
+"cic:/matita/arithmetics/nat/not_le_to_leb_false.con"