X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Fleq_leq.ma;h=d07a5f2e6b977adb4dbf42b47279b212d8276faa;hb=944b1f7b762774a6f8d99a2c2846f865b6788712;hp=1a20955176d6e0b497e4721c406efed6983a856c;hpb=90dd88139a78b4dd650d5c462ecf602bf4813cd4;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma
index 1a2095517..d07a5f2e6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/ynat/ynat_plus.ma".
 include "basic_2/grammar/leq.ma".
 
 (* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
@@ -30,3 +31,19 @@ theorem leq_trans: ∀d,e. Transitive … (leq d e).
   #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by leq_succ/
 ]
 qed-.
+
+theorem leq_canc_sn: ∀d,e,L,L1,L2. L ≃[d, e] L1 → L ≃[d, e] L2 → L1 ≃[d, e] L2.
+/3 width=3 by leq_trans, leq_sym/ qed-.
+
+theorem leq_canc_dx: ∀d,e,L,L1,L2. L1 ≃[d, e] L → L2 ≃[d, e] L → L1 ≃[d, e] L2.
+/3 width=3 by leq_trans, leq_sym/ qed-.
+
+theorem leq_join: ∀L1,L2,d,i. L1 ≃[d, i] L2 →
+                  ∀e. L1 ≃[i+d, e] L2 → L1 ≃[d, i+e] L2.
+#L1 #L2 #d #i #H elim H -L1 -L2 -d -i //
+[ #I #L1 #L2 #V #e #_ #IHL12 #e #H
+  lapply (leq_inv_succ … H ?) -H // >ypred_succ /3 width=1 by leq_pair/
+| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #e #H
+  lapply (leq_inv_succ … H ?) -H // >yplus_succ2 >ypred_succ /3 width=1 by leq_succ/
+]
+qed-.