"cic:/matita/arithmetics/nat/f_ind.con"
"cic:/matita/arithmetics/nat/f2_ind.con"
"cic:/matita/arithmetics/nat/f3_ind.con"
-
-####################################
-
-"cic:/matita/arithmetics/nat/lt_plus_Sn_r.con"
-"cic:/matita/arithmetics/nat/lt_plus_to_lt_l.con"
+#
"cic:/matita/arithmetics/nat/monotonic_lt_plus_l.con"
"cic:/matita/arithmetics/nat/monotonic_lt_plus_r.con"
-
-"cic:/matita/arithmetics/nat/le_pred_n.con"
+"cic:/matita/arithmetics/nat/lt_plus_Sn_r.con"
+"cic:/matita/arithmetics/nat/lt_plus_to_lt_l.con"
+#
"cic:/matita/arithmetics/nat/pred.con"
+#
"cic:/matita/arithmetics/nat/pred_Sn.con"
-"cic:/matita/arithmetics/nat/S_pred.con"
+#
+"cic:/matita/arithmetics/nat/le_pred_n.con"
"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"