{A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A) : int_iter f (int_succ n) a = int_iter f n (f a). Proof. induction n as [|n|n]. - reflexivity. - destruct n. 1: reflexivity. cbn; f_ap. - destruct n. 1: symmetry; apply eissect. rewrite int_pred_succ. apply (ap f^-1). rhs_V nrapply IHn. by destruct n. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.