(n : Int) {A} (f : A -> A) {ief ief' : IsEquiv f} : forall x, @int_iter A f ief n x = @int_iter A f ief' n x := int_iter_homotopic n f f (fun _ => idpath).
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.