]> 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 915a45dbfa2363190f3d6e466aceba866c53be19..72d09cc713713c754e9a4e0ef127b6bdfc5f7c25 100644 (file)
 #
 "cic:/matita/arithmetics/nat/max.con"
 "cic:/matita/arithmetics/nat/commutative_max.con"
-
-####################################
-
+#
 "cic:/matita/arithmetics/nat/to_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/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"