1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/ynat/ynat_lt.ma".
17 (* NATURAL NUMBERS WITH INFINITY ********************************************)
20 definition yplus: ynat → ynat → ynat ≝ λx,y. match x with
25 interpretation "ynat plus" 'plus x y = (yplus x y).
27 (* Properties on successor **************************************************)
29 lemma yplus_succ1: ∀m,n. (⫯m) + n = ⫯(m + n).
33 lemma yplus_SO1: ∀m. 1 + m = ⫯m.
37 (* Basic properties *********************************************************)
39 lemma yplus_inj: ∀m,n. yinj m + yinj n = yinj (m + n).
41 #m #IHm #n >(yplus_succ1 m) >IHm -IHm //
44 lemma yplus_Y2: ∀m. (m + ∞) = ∞.
48 lemma yplus_comm: commutative … yplus.
49 * [ #m ] * [1,3: #n ] //
50 normalize >ysucc_iter_Y //
53 lemma yplus_assoc: associative … yplus.
55 #y #z >yplus_inj whd in ⊢ (??%%); >iter_plus //