{A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A) : int_iter f (int_pred n) a = int_iter f n (f^-1 a). Proof. lhs_V exact (int_iter_neg f^-1 (n.-1) a). rhs_V exact (int_iter_neg f^-1 n (f^-1 a)). rewrite int_neg_pred. apply int_iter_succ_r. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.