lemma niter_zero (A) (f) (a): a = (f^{A}๐) a.
// qed.
-lemma niter_inj (A) (f) (p): f^p รข\89\90 f^{A}(ninj p).
+lemma niter_inj (A) (f) (p): f^p รข\8a\9c f^{A}(ninj p).
// qed.
(* Advanced constructions ***************************************************)
(*** iter_n_Sm *)
-lemma niter_appl (A) (f) (n): f รข\88\98 f^n รข\89\90 f^{A}n โ f.
+lemma niter_appl (A) (f) (n): f รข\88\98 f^n รข\8a\9c f^{A}n โ f.
#A #f * //
#p @exteq_repl
/2 width=5 by piter_appl, compose_repl_fwd_dx/
qed.
lemma niter_compose (A) (B) (f) (g) (h) (n):
- h รข\88\98 f รข\89\90 g รข\88\98 h รข\86\92 h รข\88\98 (f^{A}n) รข\89\90 (g^{B}n) โ h.
+ h รข\88\98 f รข\8a\9c g รข\88\98 h รข\86\92 h รข\88\98 (f^{A}n) รข\8a\9c (g^{B}n) โ h.
#A #B #f #g #h * //
#p #H @exteq_repl
/2 width=5 by piter_compose, compose_repl_fwd_dx/