update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / nap.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
index 921863e5065948b5b73449c61337a28d4c04ea85..6bd5d7715f82c84d491a6b6287d04173d745e9b3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
@@ -1,9 +1,10 @@
 include "ground/relocation/tr_uni_pap.ma".
 include "ground/relocation/tr_compose_pap.ma".
 include "ground/relocation/tr_pap_eq.ma".
+include "ground/relocation/tr_pap_hdtl_eq.ma".
 include "ground/notation/functions/atsection_2.ma".
 include "ground/arith/nat_lt.ma".
-include "ground/arith/nat_plus_rplus.ma".
+include "ground/arith/nat_plus_pplus.ma".
 include "ground/arith/nat_pred_succ.ma".
 
 lemma nlt_npsucc_bi (n1) (n2):
@@ -61,3 +62,34 @@ theorem tr_nap_eq_repl (i):
 <tr_nap_unfold <tr_nap_unfold
 /3 width=1 by tr_pap_eq_repl, eq_f/
 qed.
+
+lemma tr_eq_inv_nap_zero_tl_bi (f1) (f2):
+      f1＠§❨𝟎❩ = f2＠§❨𝟎❩ → ⇂f1 ≗ ⇂f2 → f1 ≗ f2.
+#f1 #f2
+<tr_nap_unfold <tr_nap_unfold #H1 #H2
+/3 width=1 by tr_eq_inv_pap_unit_tl_bi, eq_inv_pnpred_bi/
+qed-.
+
+lemma tr_nap_plus_sn (f) (m) (n):
+      (⫯⇂*[↑n]f)＠§❨m❩+f＠§❨n❩ = f＠§❨m+n❩.
+#f #m @(nat_ind_succ … m) -m [| #m #_ ] #n
+[ <nplus_zero_sn <nplus_zero_sn //
+| <tr_nap_push <nplus_comm in ⊢ (???%);
+  <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
+  <nsucc_pnpred <nrplus_inj_sn <nrplus_pnpred_dx
+  >nrplus_npsucc_sn <nrplus_inj_dx
+  <pplus_comm in ⊢ (???%); <tr_pap_plus //
+]
+qed.
+
+lemma tr_nap_plus_dx (f) (m) (n):
+      ⇂*[n]f＠§❨m❩+(⫯f)＠§❨n❩ = f＠§❨m+n❩.
+#f #m #n @(nat_ind_succ … n) -n [| #n #_ ]
+[ //
+| <tr_nap_push
+  <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
+  <nsucc_pnpred <nplus_pnpred_sn
+  >nrplus_npsucc_sn <nrplus_inj_dx
+  <tr_pap_plus //
+]
+qed.