definition niter (n:nat) (A:Type[0]) (f:A→A) (a:A) ≝
match n with
[ nzero ⇒ a
-| ninj p ⇒ f^{A}p a
+| ninj p ⇒ (f^{A}p) a
]
.
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/