wip ....

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / relocation / tr_minus_pap.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma
index f27e43c65e9effc8d30acca4230e3160eeb4bd1c..0df2d501f3734433ca2456ec7f822b6579aae978 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma
@@ -16,6 +16,7 @@ include "delayed_updating/relocation/tr_minus_pn.ma".
 include "ground/relocation/tr_pap_pn.ma".
 include "ground/relocation/tr_pap_lt.ma".
 include "ground/arith/nat_rplus_succ.ma".
+include "ground/arith/nat_minus_pminus.ma".
 include "ground/arith/pnat_le.ma".
 
 (* RIGHT SUBTRACTION FOR TOTAL RELOCATION MAPS ******************************)
@@ -42,3 +43,26 @@ lemma tr_pap_minus_le (n) (p) (f):
   ]
 ]
 qed-.
+
+lemma tr_pap_minus_ge (n:nat) (p:pnat) (f):
+      p + n ≤ f＠⧣❨p❩ →
+      f＠⧣❨p❩-n = (f-n)＠⧣❨p❩.
+#n @(nat_ind_succ … n) -n [| #n #IHn ]
+[ #p #f #_ //
+| #p elim p -p [| #p #IHp ]
+  #f elim (tr_map_split f) * #g #H0 destruct
+  [ <tr_cons_pap_unit <nrplus_unit_sn #H0
+    elim (ple_inv_succ_unit … H0)
+  |2,4:
+    <tr_pap_next <nrplus_succ_dx #Hf
+    lapply (ple_inv_succ_bi … Hf) -Hf #Hf
+    <tr_minus_next_succ >nsucc_inj /2 width=1 by/
+  | <tr_minus_push_succ <tr_pap_push <tr_pap_push <nrplus_succ_sn #Hf
+    lapply (ple_inv_succ_bi … Hf) -Hf #Hf
+    >nsucc_inj >nsucc_inj <IHp -IHp //
+    <nminus_inj_bi
+    [ <nminus_inj_bi 
+      [ <nsucc_inj @eq_f
+(*
+    <nminus_succ_sn //
+*)