From 21de0d35017656c5a55528390b54b0b2ae395b44 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 8 Jan 2021 17:06:39 +0100
Subject: [PATCH] =?utf8?q?arithmetics=20for=20=CE=BB=CE=B4?=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit

+ advances on maximum for non-negative integers
+ part of nat.ma used by λδ covered in full
+ minor additions and corrections
---
 .../lambdadelta/ground/arith/arith.txt        | 258 ++++++++++++++++++
 .../contribs/lambdadelta/ground/arith/nat.txt |  14 +-
 .../lambdadelta/ground/arith/nat_iter.ma      |   7 +-
 .../lambdadelta/ground/arith/nat_le.ma        |  15 +-
 .../lambdadelta/ground/arith/nat_le_max.ma    |  60 ++++
 .../lambdadelta/ground/arith/nat_le_minus.ma  |   6 +-
 .../ground/arith/nat_le_minus_plus.ma         |   2 +-
 .../lambdadelta/ground/arith/nat_le_plus.ma   |   2 +-
 .../lambdadelta/ground/arith/nat_le_pred.ma   |   6 +-
 .../lambdadelta/ground/arith/nat_lt.ma        |  18 +-
 .../lambdadelta/ground/arith/nat_lt_minus.ma  |  20 +-
 .../lambdadelta/ground/arith/nat_lt_pred.ma   |   2 +-
 .../lambdadelta/ground/arith/nat_lt_tri.ma    |  32 +++
 .../lambdadelta/ground/arith/nat_max.ma       |  18 +-
 .../lambdadelta/ground/arith/nat_minus.ma     |  26 +-
 .../ground/arith/nat_minus_plus.ma            |  24 +-
 .../lambdadelta/ground/arith/nat_plus.ma      |  37 ++-
 .../lambdadelta/ground/arith/nat_pred.ma      |   2 +-
 .../lambdadelta/ground/arith/nat_pred_succ.ma |   2 +-
 .../lambdadelta/ground/arith/nat_succ.ma      |  10 +-
 .../lambdadelta/ground/arith/nat_succ_iter.ma |   3 +-
 .../lambdadelta/ground/arith/nat_succ_tri.ma  |  12 +-
 .../lambdadelta/ground/arith/nat_tri.ma       |   4 +-
 .../lambdadelta/ground/arith/pnat_iter.ma     |   5 +-
 .../lambdadelta/ground/arith/pnat_plus.ma     |   6 +-
 .../lambdadelta/ground/arith/pnat_tri.ma      |   4 +-
 .../lambdadelta/ground/web/ground_src.tbl     |   4 +-
 27 files changed, 497 insertions(+), 102 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/arith.txt
 create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_lt_tri.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith.txt b/matita/matita/contribs/lambdadelta/ground/arith/arith.txt
new file mode 100644
index 000000000..1eda6fe22
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/arith.txt
@@ -0,0 +1,258 @@
+(* Equalities ***************************************************************)
+
+lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
+// qed-.
+
+lemma plus_minus_m_m_commutative (n) (m): m ≤ n → n = m+(n-m).
+/2 width=1 by plus_minus_associative/ qed-.
+
+lemma plus_to_minus_2: ∀m1,m2,n1,n2. n1 ≤ m1 → n2 ≤ m2 →
+                       m1+n2 = m2+n1 → m1-n1 = m2-n2.
+#m1 #m2 #n1 #n2 #H1 #H2 #H
+@plus_to_minus >plus_minus_associative //
+qed-.
+
+(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
+lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
+#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
+qed-.
+
+lemma lt_succ_pred: ∀m,n. n < m → m = ↑↓m.
+#m #n #Hm >S_pred /2 width=2 by ltn_to_ltO/
+qed-.
+
+fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
+/2 width=1 by plus_minus_minus_be/ qed-.
+
+lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
+/2 by plus_minus/ qed-.
+
+lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
+/2 by plus_minus/ qed-.
+
+lemma minus_minus_comm3: ∀n,x,y,z. n-x-y-z = n-y-z-x.
+// qed.
+
+(* Properties ***************************************************************)
+
+lemma eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
+#n1 elim n1 -n1 [| #n1 #IHn1 ] * [2,4: #n2 ]
+[1,4: @or_intror #H destruct
+| elim (IHn1 n2) -IHn1 /3 width=1 by or_intror, or_introl/
+| /2 width=1 by or_introl/
+]
+qed-.
+
+lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
+#m #n elim (lt_or_ge m n) /2 width=1 by or3_intro0/
+#H elim H -m /2 width=1 by or3_intro1/
+#m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/
+qed-.
+
+lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
+/3 width=1 by monotonic_le_minus_l/ qed.
+
+lemma minus_le_trans_sn: ∀x1,x2. x1 ≤ x2 → ∀x. x1-x ≤ x2.
+/2 width=3 by transitive_le/ qed.
+
+lemma le_plus_to_minus_l: ∀a,b,c. a + b ≤ c → b ≤ c-a.
+/2 width=1 by le_plus_to_minus_r/
+qed-.
+
+lemma le_plus_to_minus_comm: ∀n,m,p. n ≤ p+m → n-p ≤ m.
+/2 width=1 by le_plus_to_minus/ qed-.
+
+lemma le_inv_S1: ∀m,n. ↑m ≤ n → ∃∃p. m ≤ p & ↑p = n.
+#m *
+[ #H lapply (le_n_O_to_eq … H) -H
+  #H destruct
+| /3 width=3 by monotonic_pred, ex2_intro/
+]
+qed-.
+
+(* Note: this might interfere with nat.ma *)
+lemma monotonic_lt_pred: ∀m,n. m < n → 0 < m → pred m < pred n.
+#m #n #Hmn #Hm whd >(S_pred … Hm)
+@le_S_S_to_le >S_pred /2 width=3 by transitive_lt/
+qed.
+
+lemma lt_S_S: ∀x,y. x < y → ↑x < ↑y.
+/2 width=1 by le_S_S/ qed.
+
+lemma lt_S: ∀n,m. n < m → n < ↑m.
+/2 width=1 by le_S/ qed.
+
+lemma monotonic_lt_minus_r:
+∀p,q,n. q < n -> q < p → n-p < n-q.
+#p #q #n #Hn #H
+lapply (monotonic_le_minus_r … n H) -H #H
+@(le_to_lt_to_lt … H) -H
+/2 width=1 by lt_plus_to_minus/
+qed.
+
+(* Inversion & forward lemmas ***********************************************)
+
+lemma lt_refl_false: ∀n. n < n → ⊥.
+#n #H elim (lt_to_not_eq … H) -H /2 width=1 by/
+qed-.
+
+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 le_dec (n) (m): Decidable (n≤m).
+#n elim n -n [ /2 width=1 by or_introl/ ]
+#n #IH * [ /3 width=2 by lt_zero_false, or_intror/ ]
+#m elim (IH m) -IH
+[ /3 width=1 by or_introl, le_S_S/
+| /4 width=1 by or_intror, le_S_S_to_le/
+]
+qed-.
+
+lemma succ_inv_refl_sn: ∀x. ↑x = x → ⊥.
+#x #H @(lt_le_false x (↑x)) //
+qed-.
+
+lemma le_plus_xSy_O_false: ∀x,y. x + S y ≤ 0 → ⊥.
+#x #y #H lapply (le_n_O_to_eq … H) -H <plus_n_Sm #H destruct
+qed-.
+
+lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
+#y #z #x elim x -x /3 width=1 by le_S_S_to_le/
+#H elim (le_plus_xSy_O_false … H)
+qed-.
+
+lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
+/2 width=4 by le_plus_xySz_x_false/ qed-.
+
+lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥.
+/2 width=4 by plus_xySz_x_false/ qed-.
+
+lemma pred_inv_fix_sn: ∀x. ↓x = x → 0 = x.
+* // #x <pred_Sn #H
+elim (succ_inv_refl_sn x) //
+qed-.
+
+lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
+// qed-.
+
+lemma discr_plus_x_xy: ∀x,y. x = x + y → y = 0.
+/2 width=2 by le_plus_minus_comm/ qed-.
+
+lemma plus2_le_sn_sn: ∀m1,m2,n1,n2. m1 + n1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
+#m1 #m2 #n1 #n2 #H #Hm
+lapply (monotonic_le_plus_l n1 … Hm) -Hm >H -H
+/2 width=2 by le_plus_to_le/
+qed-.
+
+lemma plus2_le_sn_dx: ∀m1,m2,n1,n2. m1 + n1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
+/2 width=4 by plus2_le_sn_sn/ qed-.
+
+lemma plus2_le_dx_sn: ∀m1,m2,n1,n2. n1 + m1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
+/2 width=4 by plus2_le_sn_sn/ qed-.
+
+lemma plus2_le_dx_dx: ∀m1,m2,n1,n2. n1 + m1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
+/2 width=4 by plus2_le_sn_sn/ qed-.
+
+lemma lt_S_S_to_lt: ∀x,y. ↑x < ↑y → x < y.
+/2 width=1 by le_S_S_to_le/ qed-.
+
+(* Note this should go in nat.ma *)
+lemma discr_x_minus_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
+#x @(nat_ind_plus … x) -x /2 width=1 by or_introl/
+#x #_ #y @(nat_ind_plus … y) -y /2 width=1 by or_intror/
+#y #_ >minus_plus_plus_l
+#H lapply (discr_plus_xy_minus_xz … H) -H
+#H destruct
+qed-.
+
+lemma lt_inv_O1: ∀n. 0 < n → ∃m. ↑m = n.
+* /2 width=2 by ex_intro/
+#H cases (lt_le_false … H) -H //
+qed-.
+
+lemma lt_inv_S1: ∀m,n. ↑m < n → ∃∃p. m < p & ↑p = n.
+#m * /3 width=3 by lt_S_S_to_lt, ex2_intro/
+#H cases (lt_le_false … H) -H //
+qed-.
+
+lemma lt_inv_gen: ∀y,x. x < y → ∃∃z. x ≤ z & ↑z = y.
+* /3 width=3 by le_S_S_to_le, ex2_intro/
+#x #H elim (lt_le_false … H) -H //
+qed-.
+
+lemma plus_inv_O3: ∀x,y. x + y = 0 → x = 0 ∧ y = 0.
+/2 width=1 by plus_le_0/ qed-.
+
+lemma plus_inv_S3_sn: ∀x1,x2,x3. x1+x2 = ↑x3 →
+                      ∨∨ ∧∧ x1 = 0 & x2 = ↑x3
+                       | ∃∃y1. x1 = ↑y1 & y1 + x2 = x3.
+* /3 width=1 by or_introl, conj/
+#x1 #x2 #x3 <plus_S1 #H destruct
+/3 width=3 by ex2_intro, or_intror/
+qed-.
+
+lemma plus_inv_S3_dx: ∀x2,x1,x3. x1+x2 = ↑x3 →
+                      ∨∨ ∧∧ x2 = 0 & x1 = ↑x3
+                       | ∃∃y2. x2 = ↑y2 & x1 + y2 = x3.
+* /3 width=1 by or_introl, conj/
+#x2 #x1 #x3 <plus_n_Sm #H destruct
+/3 width=3 by ex2_intro, or_intror/
+qed-.
+
+lemma zero_eq_plus: ∀x,y. 0 = x + y → 0 = x ∧ 0 = y.
+* /2 width=1 by conj/ #x #y normalize #H destruct
+qed-.
+
+lemma nat_split: ∀x. x = 0 ∨ ∃y. ↑y = x.
+* /3 width=2 by ex_intro, or_introl, or_intror/
+qed-.
+
+lemma nat_elim_le_sn (Q:relation …):
+      (∀m1,m2. (∀m. m < m2-m1 → Q (m2-m) m2) → m1 ≤ m2 → Q m1 m2) →
+      ∀n1,n2. n1 ≤ n2 → Q n1 n2.
+#Q #IH #n1 #n2 #Hn
+<(minus_minus_m_m … Hn) -Hn
+lapply (minus_le n2 n1)
+let d ≝ (n2-n1)
+@(nat_elim1 … d) -d -n1 #d
+@pull_2 #Hd
+<(minus_minus_m_m … Hd) in ⊢ (%→?); -Hd
+let n1 ≝ (n2-d) #IHd
+@IH -IH [| // ] #m #Hn
+/4 width=3 by lt_to_le, lt_to_le_to_lt/
+qed-.
+
+(* Decidability of predicates ***********************************************)
+
+lemma dec_lt (R:predicate nat):
+      (∀n. Decidable … (R n)) →
+      ∀n. Decidable … (∃∃m. m < n & R m).
+#R #HR #n elim n -n [| #n * ]
+[ @or_intror * /2 width=2 by lt_zero_false/
+| * /4 width=3 by lt_S, or_introl, ex2_intro/
+| #H0 elim (HR n) -HR
+  [ /3 width=3 by or_introl, ex2_intro/
+  | #Hn @or_intror * #m #Hmn #Hm
+    elim (le_to_or_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
+    /4 width=3 by lt_S_S_to_lt, ex2_intro/
+  ]
+]
+qed-.
+
+lemma dec_min (R:predicate nat):
+      (∀n. Decidable … (R n)) → ∀n. R n →
+      ∃∃m. m ≤ n & R m & (∀p. p < m → R p → ⊥).
+#R #HR #n
+@(nat_elim1 n) -n #n #IH #Hn
+elim (dec_lt … HR n) -HR [ -Hn | -IH ]
+[ * #p #Hpn #Hp
+  elim (IH … Hpn Hp) -IH -Hp #m #Hmp #Hm #HNm
+  @(ex3_intro … Hm HNm) -HNm
+  /3 width=3 by lt_to_le, le_to_lt_to_lt/
+| /4 width=4 by ex3_intro, ex2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
index 915a45dbf..72d09cc71 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
@@ -120,18 +120,18 @@
 #
 "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"
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
index 94875efc1..7c883976c 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
@@ -17,6 +17,7 @@ include "ground/arith/nat.ma".
 
 (* ITERATED FUNCTION FOR NON-NEGATIVE INTEGERS ******************************)
 
+(*** iter *)
 definition niter (n:nat) (A:Type[0]) (f:A→A) (a:A) ≝
 match n with
 [ nzero  ⇒ a
@@ -28,16 +29,18 @@ interpretation
   "iterated function (non-negative integers)"
   'Exp A f n = (niter n A f).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
+(*** iter_O *)
 lemma niter_zero (A) (f) (a): a = (f^{A}𝟎) a.
 // qed.
 
 lemma niter_inj (A) (f) (p) (a): f^p a = f^{A}(ninj p) a.
 // qed.
 
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
 
+(*** iter_n_Sm *)
 lemma niter_appl (A) (f) (n) (a): f (f^n a) = f^{A}n (f a).
 #A #f * //
 #p #a <niter_inj <niter_inj <piter_appl //
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
index ae98e3a5e..5f2ea334f 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
@@ -36,7 +36,7 @@ lemma nle_succ_dx_refl (m): m ≤ ↑m.
 
 (*** le_O_n *)
 lemma nle_zero_sx (m): 𝟎 ≤ m.
-#m @(nat_ind … m) -m /2 width=1 by nle_succ_dx/
+#m @(nat_ind_succ … m) -m /2 width=1 by nle_succ_dx/
 qed.
 
 (*** le_S_S *)
@@ -46,9 +46,11 @@ qed.
 
 (*** le_or_ge *)
 lemma nle_ge_dis (m) (n): ∨∨ m ≤ n | n ≤ m.
-#m @(nat_ind … m) -m [ /2 width=1 by or_introl/ ]
-#m #IH #n @(nat_ind … n) -n [ /2 width=1 by or_intror/ ]
-#n #_ elim (IH n) -IH /3 width=2 by nle_succ_bi, or_introl, or_intror/
+#m #n @(nat_ind_succ_2 … m n) -m -n
+[ /2 width=1 by or_introl/
+| /2 width=1 by or_intror/
+| #m #n * /3 width=2 by nle_succ_bi, or_introl, or_intror/
+]
 qed-.
 
 (* Basic inversions *********************************************************)
@@ -81,7 +83,7 @@ lemma nle_inv_succ_zero (m): ↑m ≤ 𝟎 → ⊥.
 /3 width=2 by nle_inv_zero_dx, eq_inv_nzero_succ/ qed-.
 
 lemma nle_inv_succ_sn_refl (m): ↑m ≤ m → ⊥.
-#m @(nat_ind … m) -m [| #m #IH ] #H
+#m @(nat_ind_succ … m) -m [| #m #IH ] #H
 [ /3 width=2 by nle_inv_zero_dx, eq_inv_nzero_succ/
 | /3 width=1 by nle_inv_succ_bi/
 ]
@@ -98,11 +100,12 @@ qed-.
 
 (* Advanced eliminations ****************************************************)
 
+(*** le_elim *)
 lemma nle_ind_alt (Q: relation2 nat nat):
       (∀n. Q (𝟎) (n)) →
       (∀m,n. m ≤ n → Q m n → Q (↑m) (↑n)) →
       ∀m,n. m ≤ n → Q m n.
-#Q #IH1 #IH2 #m #n @(nat_ind_2 … m n) -m -n //
+#Q #IH1 #IH2 #m #n @(nat_ind_succ_2 … m n) -m -n //
 [ #m #H elim (nle_inv_succ_zero … H)
 | /4 width=1 by nle_inv_succ_bi/
 ]
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma
new file mode 100644
index 000000000..4f7886aa1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground/arith/nat_max.ma".
+include "ground/arith/nat_le.ma".
+
+(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
+
+(* Basic constructions with nmax ********************************************)
+
+(*** to_max *)
+lemma nle_max_sn (n):
+      ∀m1. m1 ≤ n → ∀m2. m2 ≤ n → (m1 ∨ m2) ≤ n.
+#n #m1 #H @(nle_ind_alt … H) -n -m1 //
+#n #m1 #Hnm1 #IH #m2 @(nat_ind_succ … m2) -m2
+[ #_ -IH /3 width=1 by nle_succ_bi/
+| #m2 #_ #H -Hnm1 /4 width=1 by nle_inv_succ_bi, nle_succ_bi/
+]
+qed.
+
+lemma nle_max_dx_refl_sn (m) (n): m ≤ (m ∨ n).
+#m #n @(nat_ind_succ_2 … m n) -m -n //
+#m #n #IH <nmax_succ_bi /2 width=1 by nle_succ_bi/
+qed.
+
+lemma nle_max_dx_refl_dx (m) (n): n ≤ (m ∨ n).
+#m #n @(nat_ind_succ_2 … n m) -m -n //
+#m #n #IH <nmax_succ_bi /2 width=1 by nle_succ_bi/
+qed.
+
+(* Basic destructions with nmax *********************************************)
+
+(*** le_maxl *)
+lemma nle_des_max_sn_sn (m1) (m2) (n): (m1 ∨ m2) ≤ n → m1 ≤ n.
+/2 width=3 by nle_trans/ qed-.
+
+(*** le_maxr *)
+lemma nle_des_max_sn_dx (m1) (m2) (n): (m1 ∨ m2) ≤ n → m2 ≤ n.
+/2 width=3 by nle_trans/ qed-.
+
+(* Advanced constructions with nmax *****************************************)
+
+(*** max_S1_le_S *)
+lemma nle_max_sn_succ_sn (m1) (m2) (n): (m1 ∨ m2) ≤ n → (↑m1 ∨ m2) ≤ ↑n.
+/4 width=2 by nle_des_max_sn_sn, nle_des_max_sn_dx, nle_max_sn, nle_succ_bi, nle_succ_dx/ qed.
+
+(*** max_S2_le_S *)
+lemma nle_max_sn_succ_dx (m1) (m2) (n): (m1 ∨ m2) ≤ n → (m1 ∨ ↑m2) ≤ ↑n.
+/4 width=2 by nle_des_max_sn_sn, nle_des_max_sn_dx, nle_max_sn, nle_succ_bi, nle_succ_dx/ qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma
index 607a9135e..5656acffd 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma
@@ -21,7 +21,7 @@ include "ground/arith/nat_le_pred.ma".
 
 (*** minus_le *)
 lemma nle_minus_sn_refl_sn (m) (n): m - n ≤ m.
-#m #n elim n -n //
+#m #n @(nat_ind_succ … n) -n //
 #n #IH /2 width=3 by nle_trans/
 qed.
 
@@ -30,13 +30,13 @@ lemma nle_minus_succ_sn (m) (n): ↑n - m ≤ ↑(n - m).
 
 (*** inv_eq_minus_O *)
 lemma nle_eq_minus_O (m) (n): 𝟎 = m - n → m ≤ n.
-#m #n @(nat_ind_2 … m n) //
+#m #n @(nat_ind_succ_2 … m n) //
 /3 width=1 by nle_succ_bi/
 qed.
 
 (*** monotonic_le_minus_l *)
 lemma nle_minus_sn_bi (m) (n) (o): m ≤ n → m-o ≤ n-o.
-#m #n #o elim o -o //
+#m #n #o @(nat_ind_succ … o) -o //
 #o #IH #Hmn /3 width=1 by nle_pred_bi/
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.ma
index d569e0cb3..a059c04e0 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.ma
@@ -22,7 +22,7 @@ include "ground/arith/nat_le_minus.ma".
 
 (*** le_plus_minus_m_m *)
 lemma nle_plus_minus_sn_refl_sn (n) (m): m ≤ m - n + n.
-#n elim n -n //
+#n @(nat_ind_succ … n) -n //
 #n #IH #m <nminus_succ_dx_pred_sn <nplus_succ_dx
 /2 width=1 by nle_inv_pred_sn/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
index 37a0efbb2..bbca72f27 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
@@ -61,7 +61,7 @@ lemma nle_inv_plus_zero (m) (n): m + n ≤ 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n.
 
 (*** le_plus_to_le_r *)
 lemma nle_inv_plus_bi_dx (o) (m) (n): n + o ≤ m + o → n ≤ m.
-#o @(nat_ind … o) -o /3 width=1 by nle_inv_succ_bi/
+#o @(nat_ind_succ … o) -o /3 width=1 by nle_inv_succ_bi/
 qed-.
 
 (*** le_plus_to_le *)
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma
index 75cd4bf7e..0454acee0 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma
@@ -20,7 +20,7 @@ include "ground/arith/nat_le.ma".
 (* Destructions with npred **************************************************)
 
 lemma nle_inv_pred_sn (m) (n): ↓m ≤ n → m ≤ ↑n.
-#m #n elim m -m
+#m #n @(nat_ind_succ … m) -m
 /2 width=1 by nle_succ_bi/
 qed-.
 
@@ -31,7 +31,7 @@ lemma nle_succ_pred_dx_refl (m): m ≤ ↑↓m.
 
 (*** le_pred_n *)
 lemma nle_pred_sn_refl (m): ↓m ≤ m.
-#m elim m -m //
+#m @(nat_ind_succ … m) -m //
 qed.
 
 (*** monotonic_pred *)
@@ -41,6 +41,6 @@ lemma nle_pred_bi (m) (n): m ≤ n → ↓m ≤ ↓n.
 qed.
 
 lemma nle_pred_sn (m) (n): m ≤ ↑n → ↓m ≤ n.
-#m #n elim m -m //
+#m #n @(nat_ind_succ … m) -m //
 /2 width=1 by nle_pred_bi/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
index a8ffe2e4c..48bdf9194 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
@@ -66,11 +66,15 @@ qed.
 lemma nlt_le_trans (o) (m) (n): m < o → o ≤ n → m < n.
 /2 width=3 by nle_trans/ qed-.
 
+(*** le_to_lt_to_lt *)
 lemma le_nlt_trans (o) (m) (n): m ≤ o → o < n → m < n.
 /3 width=3 by nle_succ_bi, nle_trans/ qed-.
 
 (* Basic inversions *********************************************************)
 
+lemma nlt_inv_succ_bi (m) (n): ↑m < ↑n → m < n.
+/2 width=1 by nle_inv_succ_bi/ qed-.
+
 (*** lt_to_not_le *)
 lemma nlt_ge_false (m) (n): m < n → n ≤ m → ⊥.
 /3 width=4 by nle_inv_succ_sn_refl, nlt_le_trans/ qed-.
@@ -102,7 +106,7 @@ theorem nlt_trans: Transitive … nlt.
 
 lemma nat_ind_lt_le (Q:predicate …):
       (∀n. (∀m. m < n → Q m) → Q n) → ∀n,m. m ≤ n → Q m.
-#Q #H1 #n @(nat_ind … n) -n
+#Q #H1 #n @(nat_ind_succ … n) -n
 [ #m #H <(nle_inv_zero_dx … H) -m
   @H1 -H1 #o #H elim (nlt_inv_zero_dx … H)
 | /5 width=3 by nlt_le_trans, nle_inv_succ_bi/
@@ -113,3 +117,15 @@ qed-.
 lemma nat_ind_lt (Q:predicate …):
       (∀n. (∀m. m < n → Q m) → Q n) → ∀n. Q n.
 /4 width=2 by nat_ind_lt_le/ qed-.
+
+(*** lt_elim *)
+lemma nlt_ind_alt (Q: relation2 nat nat):
+      (∀n. Q (𝟎) (↑n)) →
+      (∀m,n. m < n → Q m n → Q (↑m) (↑n)) →
+      ∀m,n. m < n → Q m n.
+#Q #IH1 #IH2 #m #n @(nat_ind_succ_2 … n m) -m -n //
+[ #m #H
+  elim (nlt_inv_zero_dx … H)
+| /4 width=1 by nlt_inv_succ_bi/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma
index bf889def7..79b8f1a0b 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma
@@ -17,16 +17,6 @@ include "ground/arith/nat_lt_pred.ma".
 
 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
 
-(* Rewrites with nminus *****************************************************)
-
-(*** minus_pred_pred *)
-lemma nminus_pred_bi (m) (n): 𝟎 < m → 𝟎 < n → n - m = ↓n - ↓m.
-#m #n #Hm #Hn
->(nlt_inv_zero_sn … Hm) in ⊢ (??%?); -Hm
->(nlt_inv_zero_sn … Hn) in ⊢ (??%?); -Hn
-//
-qed-.
-
 (* Constructions with nminus ************************************************)
 
 (*** monotonic_lt_minus_l *)
@@ -38,8 +28,16 @@ qed.
 
 (* Destructions with nminus *************************************************)
 
+(*** minus_pred_pred *)
+lemma nminus_pred_bi (m) (n): 𝟎 < m → 𝟎 < n → n - m = ↓n - ↓m.
+#m #n #Hm #Hn
+>(nlt_inv_zero_sn … Hm) in ⊢ (??%?); -Hm
+>(nlt_inv_zero_sn … Hn) in ⊢ (??%?); -Hn
+//
+qed-.
+
 lemma nlt_des_minus_dx (o) (m) (n): m < n - o → o < n.
-#o elim o -o
+#o @(nat_ind_succ … o) -o
 [ #m #n <nminus_zero_dx
   /2 width=3 by le_nlt_trans/
 | #o #IH #m #n <nminus_succ_dx_pred_sn #H
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma
index 7ebc811f8..c319006fc 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma
@@ -26,7 +26,7 @@ lemma nlt_zero_sn (m): m = ↑↓m → 𝟎 < m.
 
 (*** S_pred *)
 lemma nlt_inv_zero_sn (m): 𝟎 < m → m = ↑↓m.
-#m @(nat_ind … m) -m //
+#m @(nat_ind_succ … m) -m //
 #H elim (nlt_inv_refl … H)
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_tri.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_tri.ma
new file mode 100644
index 000000000..ef29ded8c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_tri.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground/arith/nat_succ_tri.ma".
+include "ground/arith/nat_lt.ma".
+
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
+
+(* Destructions with ntri ***************************************************)
+
+(*** tri_lt *)
+lemma ntri_lt (A) (a1) (a2) (a3) (n1) (n2):
+      n1 < n2 → a1 = ntri A n1 n2 a1 a2 a3.
+#A #a1 #a2 #a3 #n1 #n2 #H @(nlt_ind_alt … H) -H //
+qed-.
+
+(*** tri_gt *)
+lemma ntri_gt (A) (a1) (a2) (a3) (n1) (n2):
+      n2 < n1 → a3 = ntri A n1 n2 a1 a2 a3.
+#A #a1 #a2 #a3 #n1 #n2 #H @(nlt_ind_alt … H) -H //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
index 0032637b1..4e1e88280 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
@@ -25,7 +25,7 @@ interpretation
   "maximum (non-negative integers)"
   'or m n = (nmax m n).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** max_O1 *)
 lemma nmax_zero_sn (n2): n2 = (𝟎 ∨ n2).
@@ -44,7 +44,7 @@ lemma nmax_succ_bi (n1) (n2): ↑(n1 ∨ n2) = (↑n1 ∨ ↑n2).
 <ntri_f_tri //
 qed.
 
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
 
 (*** idempotent_max *)
 lemma nmax_idem (n): n = (n ∨ n).
@@ -52,22 +52,20 @@ lemma nmax_idem (n): n = (n ∨ n).
 
 (*** commutative_max *)
 lemma nmax_comm: commutative … nmax.
-#m #n @(nat_ind_2 … m n) -m -n //
+#m #n @(nat_ind_succ_2 … m n) -m -n //
 qed-.
 
 (*** associative_max *)
 lemma nmax_assoc: associative … nmax.
-#n1 elim n1 -n1 //
-#n1 #IH #n2 elim n2 -n2 //
-#n2 #_ #n3 elim n3 -n3 //
-qed-.
+#n1 #n2 @(nat_ind_succ_2 … n1 n2) -n1 -n2 //
+#n1 #n2 #IH #n3 @(nat_ind_succ … n3) -n3 //
+qed.
 
 (* Basic inversions *********************************************************)
 
 (*** max_inv_O3 *)
 lemma nmax_inv_zero (n1) (n2): 𝟎 = (n1 ∨ n2) → ∧∧ 𝟎 = n1 & 𝟎 = n2.
-#n1 elim n1 -n1 [ /2 width=1 by conj/ ]
-#n1 #_ #n2 elim n2 -n2 [ /2 width=1 by conj/ ]
-#n2 #_ <nmax_succ_bi #H
+#n1 #n2 @(nat_ind_succ_2 … n1 n2) -n1 -n2 /2 width=1 by conj/
+#n1 #n2 #_ <nmax_succ_bi #H
 elim (eq_inv_nzero_succ … H)
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
index 788435570..f386d413a 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
@@ -25,47 +25,51 @@ interpretation
   "minus (positive integers)"
   'minus m n = (nminus m n).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** minus_n_O *)
 lemma nminus_zero_dx (m): m = m - 𝟎.
 // qed.
 
-lemma nminus_pred_sn (m) (n): ↓(m - n) = ↓m - n.
-#m #n @(niter_appl … npred)
-qed.
+(*** minus_SO_dx *)
+lemma nminus_one_dx (m): ↓m = m - 𝟏 .
+// qed.
 
 (*** eq_minus_S_pred *)
 lemma nminus_succ_dx (m) (n): ↓(m - n) = m - ↑n.
 #m #n @(niter_succ … npred)
 qed.
 
+(* Advanced constructions ***************************************************)
+
+lemma nminus_pred_sn (m) (n): ↓(m - n) = ↓m - n.
+#m #n @(niter_appl … npred)
+qed.
+
 (*** minus_O_n *)
 lemma nminus_zero_sn (n): 𝟎 = 𝟎 - n.
-#n elim n -n //
+#n @(nat_ind_succ … n) -n //
 qed.
 
 (*** minus_S_S *)
 lemma nminus_succ_bi (m) (n): m - n = ↑m - ↑n.
-#m #n elim n -n //
+#m #n @(nat_ind_succ … n) -n //
 qed.
 
-(* Advanced rewrites ********************************************************)
-
 lemma nminus_succ_dx_pred_sn (m) (n): ↓m - n = m - ↑n.
 // qed-.
 
 (*** minus_n_n *)
 lemma nminus_refl (m): 𝟎 = m - m.
-#m elim m -m //
+#m @(nat_ind_succ … m) -m //
 qed.
 
 (*** minus_Sn_n *)
 lemma nminus_succ_sn_refl (m): ninj (𝟏) = ↑m - m.
-#m elim m -m //
+#m @(nat_ind_succ … m) -m //
 qed.
 
 (*** minus_minus_comm *)
 lemma nminus_minus_comm (o) (m) (n): o - m - n = o - n - m.
-#o #m #n elim n -n //
+#o #m #n @(nat_ind_succ … n) -n //
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma
index bf5cf5fee..3e018b775 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma
@@ -17,11 +17,11 @@ include "ground/arith/nat_minus.ma".
 
 (* SUBTRACTION FOR NON-NEGATIVE INTEGERS ************************************)
 
-(* Rewrites with nplus ******************************************************)
+(* Constructions with nplus *************************************************)
 
 (*** minus_plus_m_m *)
 lemma nminus_plus_sn_refl_sn (m) (n): m = m + n - n.
-#m #n elim n -n //
+#m #n @(nat_ind_succ … n) -n //
 #n #IH <nplus_succ_dx <nminus_succ_bi //
 qed.
 
@@ -31,7 +31,7 @@ qed.
 
 (*** minus_plus *)
 theorem nminus_plus_assoc (o) (m) (n): o-m-n = o-(m+n).
-#o #m #n elim n -n //
+#o #m #n @(nat_ind_succ … n) -n //
 #n #IH <nplus_succ_dx <nminus_succ_dx <nminus_succ_dx //
 qed-.
 
@@ -62,17 +62,15 @@ lemma eq_inv_plus_nminus_refl_sn (m) (n) (o):
       m + o = m - n →
       ∨∨ ∧∧ 𝟎 = m & 𝟎 = o
        | ∧∧ 𝟎 = n & 𝟎 = o.
-#m elim m -m
+#m #n @(nat_ind_succ_2 … m n) -m -n
 [ /3 width=1 by or_introl, conj/
-| #m #IH #n @(nat_ind … n) -n
-  [ #o #Ho
-    lapply (eq_inv_nplus_bi_sn … (𝟎) Ho) -Ho
-    /3 width=1 by or_intror, conj/
-  | #n #_ #o
-    <nminus_succ_bi >nplus_succ_shift #Ho
-    elim (IH … Ho) -IH -Ho * #_ #H
-    elim (eq_inv_nzero_succ … H)
-  ]
+| #m #o #Ho
+  lapply (eq_inv_nplus_bi_sn … (𝟎) Ho) -Ho
+  /3 width=1 by or_intror, conj/
+| #m #n #IH #o
+  <nminus_succ_bi >nplus_succ_shift #Ho
+  elim (IH … Ho) -IH -Ho * #_ #H
+  elim (eq_inv_nzero_succ … H)
 ]
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index d9c82ae33..f7d79ccdf 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
@@ -24,22 +24,32 @@ interpretation
   "plus (positive integers)"
   'plus m n = (nplus m n).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** plus_n_O *)
 lemma nplus_zero_dx (m): m = m + 𝟎.
 // qed.
 
+(*** plus_SO_dx *)
 lemma nplus_one_dx (n): ↑n = n + 𝟏.
 // qed.
 
-(* Advanved rewrites (semigroup properties) *********************************)
-
 (*** plus_n_Sm *)
 lemma nplus_succ_dx (m) (n): ↑(m+n) = m + ↑n.
 #m #n @(niter_succ … nsucc)
 qed.
 
+(* Constructions with niter *************************************************)
+
+(*** iter_plus *)
+lemma niter_plus (A) (f) (a) (n1) (n2):
+      f^n1 (f^n2 a) = f^{A}(n1+n2) a.
+#A #f #a #n1 #n2 @(nat_ind_succ … n2) -n2 //
+#n2 #IH <nplus_succ_dx <niter_succ <niter_succ <niter_appl //
+qed.
+
+(* Advanved constructions (semigroup properties) ****************************)
+
 (*** plus_S1 *)
 lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.
 #m #n @(niter_appl … nsucc)
@@ -47,22 +57,23 @@ qed.
 
 (*** plus_O_n.con *)
 lemma nplus_zero_sn (m): m = 𝟎 + m.
-#m @(nat_ind … m) -m //
+#m @(nat_ind_succ … m) -m //
 qed.
 
 (*** commutative_plus *)
 lemma nplus_comm: commutative … nplus.
-#m @(nat_ind … m) -m //
+#m @(nat_ind_succ … m) -m //
 qed-.
 
 (*** associative_plus *)
 lemma nplus_assoc: associative … nplus.
-#m #n #o @(nat_ind … o) -o //
+#m #n #o @(nat_ind_succ … o) -o //
 #o #IH <nplus_succ_dx <nplus_succ_dx <nplus_succ_dx <IH -IH //
 qed.
 
-(* Advanced constructions ***************************************************)
+(* Helper constructions *****************************************************)
 
+(*** plus_SO_sn *)
 lemma nplus_one_sn (n): ↑n = 𝟏 + n.
 #n <nplus_comm // qed.
 
@@ -81,14 +92,16 @@ qed-.
 (* Basic inversions *********************************************************)
 
 lemma eq_inv_nzero_plus (m) (n): 𝟎 = m + n → ∧∧ 𝟎 = m & 𝟎 = n.
-#m #n @(nat_ind … n) -n /2 width=1 by conj/
-#n #_ <nplus_succ_dx #H
-elim (eq_inv_nzero_succ … H)
+#m #n @(nat_ind_succ … n) -n
+[ /2 width=1 by conj/
+| #n #_ <nplus_succ_dx #H
+  elim (eq_inv_nzero_succ … H)
+]
 qed-.
 
 (*** injective_plus_l *)
 lemma eq_inv_nplus_bi_dx (o) (m) (n): m + o = n + o → m = n.
-#o @(nat_ind … o) -o /3 width=1 by eq_inv_nsucc_bi/
+#o @(nat_ind_succ … o) -o /3 width=1 by eq_inv_nsucc_bi/
 qed-.
 
 (*** injective_plus_r *)
@@ -102,5 +115,5 @@ qed-.
 (*** nat_ind_plus *)
 lemma nat_ind_plus (Q:predicate …):
       Q (𝟎) → (∀n. Q n → Q (𝟏+n)) → ∀n. Q n.
-#Q #IH1 #IH2 #n @(nat_ind … n) -n /2 width=1 by/
+#Q #IH1 #IH2 #n @(nat_ind_succ … n) -n /2 width=1 by/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
index 3d6655065..fb196e042 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
@@ -28,7 +28,7 @@ interpretation
   "predecessor (non-negative integers)"
   'DownArrow m = (npred m).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 (*** pred_O *)
 lemma npred_zero: 𝟎 = ↓𝟎.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
index f21156455..a9a3ecd08 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
@@ -17,7 +17,7 @@ include "ground/arith/nat_pred.ma".
 
 (* PREDECESSOR FOR NON-NEGATIVE INTEGERS ************************************)
 
-(* Rewrites with nsucc ******************************************************)
+(* Constructions with nsucc *************************************************)
 
 (*** pred_Sn pred_S *)
 lemma npred_succ (n): n = ↓↑n.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
index 923b235e6..9455ca744 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
@@ -25,7 +25,7 @@ interpretation
   "successor (non-negative integers)"
   'UpArrow m = (nsucc m).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 lemma nsucc_zero: ninj (𝟏) = ↑𝟎.
 // qed.
@@ -36,20 +36,20 @@ lemma nsucc_inj (p): ninj (↑p) = ↑(ninj p).
 (* Basic eliminations *******************************************************)
 
 (*** nat_ind *)
-lemma nat_ind (Q:predicate …):
+lemma nat_ind_succ (Q:predicate …):
       Q (𝟎) → (∀n. Q n → Q (↑n)) → ∀n. Q n.
 #Q #IH1 #IH2 * //
 #p elim p -p /2 width=1 by/
 qed-.
 
 (*** nat_elim2 *)
-lemma nat_ind_2 (Q:relation2 …):
+lemma nat_ind_succ_2 (Q:relation2 …):
       (∀n. Q (𝟎) n) →
       (∀m. Q (↑m) (𝟎)) →
       (∀m,n. Q m n → Q (↑m) (↑n)) →
       ∀m,n. Q m n.
-#Q #IH1 #IH2 #IH3 #m elim m -m [ // ]
-#m #IH #n elim n -n /2 width=1 by/
+#Q #IH1 #IH2 #IH3 #m @(nat_ind_succ … m) -m [ // ]
+#m #IH #n @(nat_ind_succ … n) -n /2 width=1 by/
 qed-.
 
 (* Basic inversions ***************************************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma
index b3eee2068..63031d935 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma
@@ -17,8 +17,9 @@ include "ground/arith/nat_succ.ma".
 
 (* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
 
-(* Rewrites with niter ******************************************************)
+(* Constructions with niter *************************************************)
 
+(*** iter_S *)
 lemma niter_succ (A) (f) (n) (a): f (f^n a) = f^{A}(↑n) a.
 #A #f * //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma
index e3be44c68..b8c1191b9 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma
@@ -17,7 +17,17 @@ include "ground/arith/nat_succ.ma".
 
 (* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
 
-(* Rewrites with ntri *******************************************************)
+(* Constructions with ntri **************************************************)
+
+lemma ntri_zero_succ (A) (a1) (a2) (a3) (n):
+      a1 = ntri A (𝟎) (↑n) a1 a2 a3.
+#A #a1 #a2 #a3 * //
+qed.
+
+lemma ntri_succ_zero (A) (a1) (a2) (a3) (n):
+      a3 = ntri A (↑n) (𝟎) a1 a2 a3.
+#A #a1 #a2 #a3 * //
+qed.
 
 lemma ntri_succ_bi (A) (a1) (a2) (a3) (n1) (n2):
       ntri A (n1) (n2) a1 a2 a3 = ntri A (↑n1) (↑n2) a1 a2 a3.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma
index b5be40624..4fb5225e9 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma
@@ -25,7 +25,7 @@ definition ntri (A:Type[0]) (n1) (n2) (a1) (a2) (a3): A ≝
   | ninj  p1 ⇒ match n2 with [ nzero ⇒ a3 | ninj p2 ⇒ ptri A p1 p2 a1 a2 a3 ]
   ].
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 lemma ntri_zero_bi (A) (a1) (a2) (a3):
       a2 = ntri A (𝟎) (𝟎) a1 a2 a3.
@@ -43,7 +43,7 @@ lemma ntri_inj_bi (A) (a1) (a2) (a3) (p1) (p2):
       ptri A (p1) (p2) a1 a2 a3 = ntri A (p1) (p2) a1 a2 a3.
 // qed.
 
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
 
 (*** tri_eq *)
 lemma ntri_eq (A) (a1) (a2) (a3) (n): a2 = ntri A n n a1 a2 a3.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
index 9e806cfe2..49a51b0af 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
@@ -17,6 +17,7 @@ include "ground/arith/pnat.ma".
 
 (* ITERATED FUNCTION FOR POSITIVE INTEGERS **********************************)
 
+(* Note: see also: lib/arithemetics/bigops.ma *)
 rec definition piter (p:pnat) (A:Type[0]) (f:A→A) (a:A) ≝
 match p with
 [ punit   ⇒ f a
@@ -27,7 +28,7 @@ interpretation
   "iterated function (positive integers)"
   'Exp A f p = (piter p A f).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 lemma piter_unit (A) (f) (a): f a = (f^{A}𝟏) a.
 // qed.
@@ -35,7 +36,7 @@ lemma piter_unit (A) (f) (a): f a = (f^{A}𝟏) a.
 lemma piter_succ (A) (f) (p) (a): f (f^p a) = f^{A}(↑p) a.
 // qed.
 
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
 
 lemma piter_appl (A) (f) (p) (a): f (f^p a) = f^{A}p (f a).
 #A #f #p elim p -p //
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index e6db03ac4..c5c6ade72 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -23,7 +23,7 @@ interpretation
   "plus (positive integers)"
   'plus p q = (pplus p q).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 lemma pplus_one_dx (p): ↑p = p + 𝟏.
 // qed.
@@ -31,7 +31,7 @@ lemma pplus_one_dx (p): ↑p = p + 𝟏.
 lemma pplus_succ_dx (p) (q): ↑(p+q) = p + ↑q.
 // qed.
 
-(* Advanced reweites (semigroup properties) *********************************)
+(* Advanced constructions (semigroup properties) ****************************)
 
 lemma pplus_succ_sn (p) (q): ↑(p+q) = ↑p + q.
 #p #q @(piter_appl … psucc)
@@ -43,7 +43,7 @@ qed.
 
 lemma pplus_comm: commutative … pplus.
 #p elim p -p //
-qed.
+qed-.
 
 lemma pplus_assoc: associative … pplus.
 #p #q #r elim r -r //
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma
index 617849d8f..e60f3f969 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma
@@ -22,7 +22,7 @@ rec definition ptri (A:Type[0]) p1 p2 a1 a2 a3 on p1 : A ≝
   | psucc p1 ⇒ match p2 with [ punit ⇒ a3 | psucc p2 ⇒ ptri A p1 p2 a1 a2 a3 ]
   ].
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 lemma ptri_unit_bi (A) (a1) (a2) (a3):
       a2 = ptri A (𝟏) (𝟏) a1 a2 a3.
@@ -40,7 +40,7 @@ lemma ptri_succ_bi (A) (a1) (a2) (a3) (p1) (p2):
       ptri A (p1) (p2) a1 a2 a3 = ptri A (↑p1) (↑p2) a1 a2 a3.
 // qed.
 
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
 
 lemma ptri_eq (A) (a1) (a2) (a3) (p): a2 = ptri A p p a1 a2 a3.
 #A #a1 #a2 #a3 #p elim p -p //
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index ce8d9855c..fbe22cf2e 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -59,8 +59,8 @@ table {
   class "grass"
   [ { "arithmetics" * } {
       [ { "non-negative integers" * } {
-          [ "nat_lt ( ?&lt;? )" "nat_lt_pred" "nat_lt_plus" "nat_lt_minus" "nat_lt_minus_plus" * ]
-          [ "nat_le ( ?≤? )" "nat_le_pred" "nat_le_plus" "nat_le_minus" "nat_le_minus_plus" * ]
+          [ "nat_lt ( ?&lt;? )" "nat_lt_tri" "nat_lt_pred" "nat_lt_plus" "nat_lt_minus" "nat_lt_minus_plus" * ]
+          [ "nat_le ( ?≤? )" "nat_le_pred" "nat_le_plus" "nat_le_minus" "nat_le_minus_plus" "nat_le_max" * ]
           [ "nat_max ( ?∨? )" * ]
           [ "nat_minus ( ?-? )" "nat_minus_plus" * ]
           [ "nat_plus ( ?+? )" * ]
-- 
2.39.2