{A A'} (f : A -> A) `{!IsEquiv f} (f' : A' -> A') `{!IsEquiv f'} (g : A -> A') (p : g o f == f' o g) (n : Int) (a : A) : g (int_iter f n a) = int_iter f' n (g a). Proof. induction n as [|n IHn|n IHn] in a |- *. - reflexivity. - rewrite 2 int_iter_succ_r. rewrite IHn. f_ap. - rewrite 2 int_iter_pred_r. rewrite IHn. f_ap. apply moveL_equiv_V. lhs_V nrapply p. f_ap. apply eisretr. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.