{A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A) : int_iter f (int_succ n) a = f (int_iter f n a). Proof. induction n as [|n|n]. - reflexivity. - by destruct n. - rewrite int_pred_succ. destruct n. all: symmetry; 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.