X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat.txt;h=72d09cc713713c754e9a4e0ef127b6bdfc5f7c25;hb=21de0d35017656c5a55528390b54b0b2ae395b44;hp=2bd0eabca2a0c38253dfe23fe7501864a7665e33;hpb=ccf5878f2a2ec7f952f140e162391708a740517b;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt index 2bd0eabca..72d09cc71 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt @@ -117,20 +117,21 @@ "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/to_max.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"