X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=5f8451a27216a16883d4e829526fe51d24190931;hb=5102e7f780e83c7fef1d3826f81dfd37ee4028bc;hp=b23fb9de8280f4fe9efd714c1c4462a07956c4dc;hpb=174ee1889b5c91ef5339c718d7657ed0e5da21e8;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index b23fb9de8..5f8451a27 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -12,11 +12,17 @@ (* *) (**************************************************************************) +include "ground_2/notation/functions/successor_1.ma". +include "ground_2/notation/functions/predecessor_1.ma". include "arithmetics/nat.ma". include "ground_2/lib/star.ma". (* ARITHMETICAL PROPERTIES **************************************************) +interpretation "nat successor" 'Successor m = (S m). + +interpretation "nat predecessor" 'Predecessor m = (pred m). + (* Iota equations ***********************************************************) lemma pred_O: pred 0 = 0. @@ -133,6 +139,9 @@ lemma lt_zero_false: ∀n. n < 0 → ⊥. #n #H elim (lt_to_not_le … H) -H /2 width=1 by/ qed-. +lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥. +/3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-. + lemma pred_inv_refl: ∀m. pred m = m → m = 0. * // normalize #m #H elim (lt_refl_false m) // qed-.