{A} (f : A -> A) `{IsEquiv _ _ f} (m n : Int) : int_iter f (m + n) == int_iter f m o int_iter f n. Proof. intros a. induction m as [|m|m]. - reflexivity. - rewrite int_add_succ_l. rewrite 2 int_iter_succ_l. f_ap. - rewrite int_add_pred_l. rewrite 2 int_iter_pred_l. f_ap. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.