+
+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 //
+*)