+lemma lsx_ge_up: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d + yinj e →
+ ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L → G ⊢ ⬊*[h, g, U, d] L.
+#h #g #G #L #T #U #dt #d #e #Hdtde #HTU #H @(lsx_ind … H) -L
+/5 width=7 by lsx_intro, lleq_ge_up/
+qed-.
+
+lemma lsx_ge: ∀h,g,G,L,T,d1,d2. d1 ≤ d2 →
+ G ⊢ ⬊*[h, g, T, d1] L → G ⊢ ⬊*[h, g, T, d2] L.
+#h #g #G #L #T #d1 #d2 #Hd12 #H @(lsx_ind … H) -L
+/5 width=7 by lsx_intro, lleq_ge/
+qed-.
+