+lemma coafter_tls_succ: ∀g2,g1,g. g2 ~⊚ g1 ≡ g →
+ ∀n. @⦃0, g2⦄ ≡ n → ⫱*[⫯n]g2 ~⊚ ⫱g1 ≡ ⫱*[⫯n]g.
+#g2 #g1 #g #Hg #n #Hg2
+lapply (coafter_tls … Hg2 … Hg) -Hg #Hg
+lapply (at_pxx_tls … Hg2) -Hg2 #H
+elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
+elim (coafter_inv_pxx … Hg … H2) -Hg * #f1 #f #Hf #H1 #H0 destruct
+<tls_S <tls_S <H2 <H0 -g2 -g -n //
+qed.
+
+lemma coafter_fwd_xpx_pushs: ∀g2,f1,g,n. g2 ~⊚ ↑f1 ≡ g → @⦃0, g2⦄ ≡ n →
+ ∃f. ↑*[⫯n]f = g.
+#g2 #g1 #g #n #Hg #Hg2
+elim (coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
+lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs #Hf
+lapply (at_pxx_tls … Hg2) -Hg2 #H
+elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
+elim (coafter_inv_pxx … Hf … H2) -Hf -H2 * #f1 #g #_ #H1 #H0 destruct
+[ /2 width=2 by ex_intro/
+| elim (discr_next_push … H1)
+]
+qed-.
+
+lemma coafter_fwd_xnx_pushs: ∀g2,f1,g,n. g2 ~⊚ ⫯f1 ≡ g → @⦃0, g2⦄ ≡ n →
+ ∃f. ↑*[n] ⫯f = g.
+#g2 #g1 #g #n #Hg #Hg2
+elim (coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
+lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs #Hf
+lapply (at_pxx_tls … Hg2) -Hg2 #H
+elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
+elim (coafter_inv_pxx … Hf … H2) -Hf -H2 * #f1 #g #_ #H1 #H0 destruct
+[ elim (discr_push_next … H1)
+| /2 width=2 by ex_intro/
+]
+qed-.
+