some additions ...

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 08662a4ce4cda46595ed0609ca11e13ed019f7f2..081301a52680838c8bab52cc7cb42a2fe3b8245b 100644 (file)
--- 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 c855b0dbb3d649067fadc76f7e803b1acaf582f5..f34702717fe1c8eb74ef6ce573945d37259fba0a 100644 (file)
--- 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 ef976b4add038aaa3c1db4398e2181b48b562e7d..2428caa68291969b2c02753cff2b04c8081b531b 100644 (file)
--- 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.