From 4e2cde56d7a4c30c1fa07d58f76beab22a174151 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 10 Mar 2014 19:01:45 +0000
Subject: [PATCH] some additions ...

---
 .../contribs/lambdadelta/basic_2/relocation/lleq_leq.ma   | 4 ++++
 .../lambdadelta/basic_2/relocation/llpx_sn_leq.ma         | 6 ++++++
 .../contribs/lambdadelta/ground_2/ynat/ynat_plus.ma       | 8 +++++++-
 3 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_leq.ma
index 08662a4ce..081301a52 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_leq.ma
@@ -30,3 +30,7 @@ lemma lleq_leq_trans: ∀L,L1,T,d. L ⋕[T, d] L1 →
 lemma lleq_leq_repl: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K1. K1 ≃[d, ∞] L1 →
                      ∀K2. L2 ≃[d, ∞] K2 → K1 ⋕[T, d] K2.
 /2 width=5 by llpx_sn_leq_repl/ qed-.
+
+lemma lleq_bind_repl_SO: ∀I1,I2,L1,L2,V1,V2,T. L1.ⓑ{I1}V1 ⋕[T, 0] L2.ⓑ{I2}V2 →
+                         ∀J1,J2,W1,W2. L1.ⓑ{J1}W1 ⋕[T, 1] L2.ⓑ{J2}W2.
+/2 width=5 by llpx_sn_bind_repl_SO/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_leq.ma
index c855b0dbb..f34702717 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_leq.ma
@@ -46,3 +46,9 @@ qed-.
 lemma llpx_sn_leq_repl: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → ∀K1. K1 ≃[d, ∞] L1 → 
                         ∀K2. L2 ≃[d, ∞] K2 → llpx_sn R d T K1 K2.
 /3 width=4 by llpx_sn_leq_trans, leq_llpx_sn_trans/ qed-.
+
+lemma llpx_sn_bind_repl_SO: ∀R,I1,I2,L1,L2,V1,V2,T. llpx_sn R 0 T (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) →
+                            ∀J1,J2,W1,W2. llpx_sn R 1 T (L1.ⓑ{J1}W1) (L2.ⓑ{J2}W2).
+#R #I1 #I2 #L1 #L2 #V1 #V2 #T #HT #J1 #J2 #W1 #W2 lapply (llpx_sn_ge R … 1 … HT) -HT
+/3 width=7 by llpx_sn_leq_repl, leq_succ/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
index ef976b4ad..2428caa68 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
@@ -132,7 +132,7 @@ lemma yle_fwd_plus_ge_inj: ∀m1:nat. ∀m2,n1,n2:ynat. m2 ≤ m1 → m1 + n1 
 #x #H0 #H destruct /3 width=4 by yle_fwd_plus_ge, yle_inj/
 qed-.
 
-(* Forward lemmas on strict_order *******************************************)
+(* Forward lemmas on strict order *******************************************)
 
 lemma ylt_inv_monotonic_plus_dx: ∀x,y,z. x + z < y + z → x < y.
 * [2: #y #z >yplus_comm #H elim (ylt_inv_Y1 … H) ]
@@ -142,6 +142,12 @@ qed-.
 
 (* Properties on strict order ***********************************************)
 
+lemma ylt_plus_dx1_trans: ∀x,z. z < x → ∀y. z < x + yinj y.
+/2 width=3 by ylt_yle_trans/ qed.
+
+lemma ylt_plus_dx2_trans: ∀y,z. z < y → ∀x. z < yinj x + y.
+/2 width=3 by ylt_yle_trans/ qed.
+
 lemma monotonic_ylt_plus_dx: ∀x,y. x < y → ∀z:nat. x + yinj z < y + yinj z.
 #x #y #Hxy #z elim z -z /3 width=1 by ylt_succ/
 qed.
-- 
2.39.2