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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
index 7fbb2d7b7..fc8e9e241 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
@@ -70,51 +70,56 @@
 "cic:/matita/arithmetics/nat/monotonic_pred.con"
 #
 "cic:/matita/arithmetics/nat/S_pred.con"
-
-####################################
-
-"cic:/matita/arithmetics/nat/discr_minus_x_xy.con"
-"cic:/matita/arithmetics/nat/discr_plus_xy_minus_xz.con"
-"cic:/matita/arithmetics/nat/eq_minus_O.con"
+#
+"cic:/matita/arithmetics/nat/minus.con"
+"cic:/matita/arithmetics/nat/minus_n_O.con"
 "cic:/matita/arithmetics/nat/eq_minus_S_pred.con"
+"cic:/matita/arithmetics/nat/minus_O_n.con"
+"cic:/matita/arithmetics/nat/minus_S_S.con"
+"cic:/matita/arithmetics/nat/minus_n_n.con"
+"cic:/matita/arithmetics/nat/minus_Sn_n.con"
+"cic:/matita/arithmetics/nat/minus_minus_comm.con"
+#
+"cic:/matita/arithmetics/nat/minus_plus_m_m.con"
+"cic:/matita/arithmetics/nat/minus_plus.con"
+"cic:/matita/arithmetics/nat/minus_plus_plus_l.con"
+"cic:/matita/arithmetics/nat/plus_minus_plus_plus_l.con"
+"cic:/matita/arithmetics/nat/plus_to_minus.con"
+"cic:/matita/arithmetics/nat/discr_plus_xy_minus_xz.con"
+"cic:/matita/arithmetics/nat/discr_minus_x_xy.con"
+#
+"cic:/matita/arithmetics/nat/minus_le.con"
 "cic:/matita/arithmetics/nat/inv_eq_minus_O.con"
-"cic:/matita/arithmetics/nat/le_minus_to_plus.con"
-"cic:/matita/arithmetics/nat/le_minus_to_plus_r.con"
+"cic:/matita/arithmetics/nat/monotonic_le_minus_l.con"
+"cic:/matita/arithmetics/nat/monotonic_le_minus_r.con"
+"cic:/matita/arithmetics/nat/eq_minus_O.con"
+"cic:/matita/arithmetics/nat/minus_Sn_m.con"
+"cic:/matita/arithmetics/nat/minus_minus_m_m.con"
+#
 "cic:/matita/arithmetics/nat/le_plus_minus_m_m.con"
 "cic:/matita/arithmetics/nat/le_plus_to_minus.con"
 "cic:/matita/arithmetics/nat/le_plus_to_minus_r.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/minus.con"
-"cic:/matita/arithmetics/nat/minus_le.con"
-"cic:/matita/arithmetics/nat/minus_le_minus_minus_comm.con"
+"cic:/matita/arithmetics/nat/le_inv_plus_l.con"
+"cic:/matita/arithmetics/nat/plus_minus_m_m.con"
+"cic:/matita/arithmetics/nat/le_minus_to_plus.con"
+"cic:/matita/arithmetics/nat/le_minus_to_plus_r.con"
+"cic:/matita/arithmetics/nat/plus_minus.con"
+"cic:/matita/arithmetics/nat/plus_minus_associative.con"
 "cic:/matita/arithmetics/nat/minus_minus_associative.con"
-"cic:/matita/arithmetics/nat/minus_minus_comm.con"
 "cic:/matita/arithmetics/nat/minus_minus.con"
-"cic:/matita/arithmetics/nat/minus_minus_m_m.con"
-"cic:/matita/arithmetics/nat/minus_n_n.con"
-"cic:/matita/arithmetics/nat/minus_n_O.con"
-"cic:/matita/arithmetics/nat/minus_O_n.con"
-"cic:/matita/arithmetics/nat/minus_plus.con"
-"cic:/matita/arithmetics/nat/minus_plus_m_m.con"
-"cic:/matita/arithmetics/nat/minus_plus_plus_l.con"
+"cic:/matita/arithmetics/nat/minus_le_minus_minus_comm.con"
+#
 "cic:/matita/arithmetics/nat/minus_pred_pred.con"
-"cic:/matita/arithmetics/nat/minus_Sn_m.con"
-"cic:/matita/arithmetics/nat/minus_Sn_n.con"
-"cic:/matita/arithmetics/nat/minus_S_S.con"
-"cic:/matita/arithmetics/nat/monotonic_le_minus_l.con"
-"cic:/matita/arithmetics/nat/monotonic_le_minus_r.con"
 "cic:/matita/arithmetics/nat/monotonic_lt_minus_l.con"
-"cic:/matita/arithmetics/nat/plus_minus_associative.con"
-"cic:/matita/arithmetics/nat/plus_minus.con"
-"cic:/matita/arithmetics/nat/plus_minus_m_m.con"
-"cic:/matita/arithmetics/nat/plus_minus_plus_plus_l.con"
-"cic:/matita/arithmetics/nat/plus_to_minus.con"
-"cic:/matita/arithmetics/nat/le_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/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/commutative_max.con"
 "cic:/matita/arithmetics/nat/leb.con"