(n : Int) {A} (f f' : A -> A) `{!IsEquiv f} `{!IsEquiv f'} (h : f == f') : int_iter f n == int_iter f' n := int_iter_commute_map f f' idmap h n.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.