From d85eac4e29291d854469e626381654181b0c7e87 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 18 Jan 2023 20:56:10 +0100
Subject: [PATCH] update in ground

+ some additions
+ some renaming
---
 .../lambdadelta/ground/arith/arith_2a.ma      |  2 +-
 .../lambdadelta/ground/arith/nat_minus.ma     |  8 +--
 .../ground/arith/nat_minus_plus.ma            |  2 +-
 .../lambdadelta/ground/arith/pnat_minus.ma    | 67 +++++++++++++++++++
 .../ground/relocation/tr_pap_lt.ma            | 25 +++++++
 .../lambdadelta/ground/relocation/tr_pn.ma    |  9 +++
 6 files changed, 107 insertions(+), 6 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/pnat_minus.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_lt.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
index a136174bc..114eddb1e 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
@@ -24,7 +24,7 @@ lemma plus_n_2: ∀n. (n + 𝟐) = n + 𝟏 + 𝟏.
 // qed.
 
 lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >nminus_comm <nminus_assoc_comm_23 //
+#a #b #c1 #H >nminus_comm_21 <nminus_assoc_comm_23 //
 qed-.
 
 lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
index e4ccf83f4..6f1168272 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
@@ -70,11 +70,11 @@ lemma nminus_succ_sn_refl (m): ninj (𝟏) = ↑m - m.
 qed.
 
 (*** minus_minus_comm *)
-lemma nminus_comm (o) (m) (n): o - m - n = o - n - m.
-#o #m #n @(nat_ind_succ … n) -n //
+lemma nminus_comm_21 (m) (n1) (n2): m - n1 - n2 = m - n2 - n1.
+#m #n1 #n2 @(nat_ind_succ … n2) -n2 //
 qed.
 
 (*** minus_minus_comm3 *)
-lemma nminus_comm_231 (n) (m1) (m2) (m3):
-      n-m1-m2-m3 = n-m2-m3-m1.
+lemma nminus_comm_231 (m) (n1) (n2) (n3):
+      m-n1-n2-n3 = m-n2-n3-n1.
 // 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 e910fdaa0..97c24dbd4 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma
@@ -38,7 +38,7 @@ qed.
 
 (*** minus_plus_plus_l *)
 lemma nminus_plus_dx_bi (m) (n) (o): m - n = (m + o) - (n + o).
-#m #n #o <nminus_plus_assoc <nminus_comm //
+#m #n #o <nminus_plus_assoc <nminus_comm_21 //
 qed.
 
 (* Helper constructions with nplus ******************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_minus.ma
new file mode 100644
index 000000000..389510e67
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_minus.ma
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/pnat_pred.ma".
+include "ground/arith/pnat_iter.ma".
+
+(* SUBTRACTION FOR NON-NEGATIVE INTEGERS ************************************)
+
+definition pminus: pnat → pnat → pnat ≝
+           λp,q. (ppred^q) p.
+
+interpretation
+  "minus (positive integers)"
+  'minus p q = (pminus p q).
+
+(* Basic constructions ******************************************************)
+
+lemma pminus_unit_dx (p): ↓p = p - 𝟏.
+// qed.
+
+lemma pminus_succ_dx (p) (q): ↓(p - q) = p - ↑q.
+#p #q @(piter_succ … ppred)
+qed.
+
+(* Advanced constructions ***************************************************)
+
+lemma pminus_pred_sn (p) (q): ↓(p - q) = ↓p - q.
+#p #q @(piter_appl … ppred)
+qed.
+
+lemma pminus_unit_sn (q): 𝟏 = 𝟏 - q.
+#q elim q -q //
+qed.
+
+lemma pminus_succ_bi (p) (q): p - q = ↑p - ↑q.
+#p #q elim q -q //
+qed.
+
+lemma pminus_succ_dx_pred_sn (p) (q): ↓p - q = p - ↑q.
+// qed-.
+
+lemma pminus_refl (p): 𝟏 = p - p.
+#p elim p -p //
+qed.
+
+lemma pminus_succ_sn_refl (p): 𝟏 = ↑p - p.
+#p elim p -p //
+qed.
+
+lemma pminus_comm_21 (p) (q1) (q2): p - q1 - q2 = p - q2 - q1.
+#p #q1 #q2 elim q2 -q2 //
+qed.
+
+lemma pminus_comm_231 (p) (q1) (q2) (q3):
+      p-q1-q2-q3 = p-q2-q3-q1.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_lt.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_lt.ma
new file mode 100644
index 000000000..32ce73d45
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_lt.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/tr_pap_pat.ma".
+include "ground/relocation/pr_pat_lt.ma".
+
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
+(* Constructions with plt ***************************************************)
+
+lemma tr_pap_increasing (f) (p):
+      p ≤ f＠⧣❨p❩.
+/2 width=2 by pr_pat_increasing/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma
index 2418afd11..c38aad712 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma
@@ -47,3 +47,12 @@ lemma tr_inj_push (f): ⫯𝐭❨f❩ = 𝐭❨⫯f❩.
 lemma tr_inj_next (f): ↑𝐭❨f❩ = 𝐭❨↑f❩.
 * //
 qed.
+
+(* Basic eliminations *******************************************************)
+
+lemma tr_map_split (f:tr_map):
+      ∨∨ ∃g. ⫯g = f
+       | ∃g. ↑g = f.
+* *
+/3 width=2 by ex_intro, or_introl, or_intror/
+qed-.
-- 
2.39.2