Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Spaces.Pos.
Require Import Spaces.Int.Core.
Require Import Spaces.Int.Spec.

(** ** Iteration of equivalences *)

(** *** Iteration by arbitrary integers *)

Definition int_iter {A} (f : A -> A) `{!IsEquiv f} (n : Int) : A -> A
  := match n with
      | neg n => fun x => pos_iter f^-1 n x
      | zero => idmap
      | pos n => fun x => pos_iter f n x
     end.

(** Iteration by arbitrary integers requires the endofunction to be an equivalence, so that we can define a negative iteration by using its inverse. *)


Definition int_iter_succ_l {A} (f : A -> A) `{IsEquiv _ _ f}
  (n : Int) (a : A)
  : int_iter f (int_succ n) a = f (int_iter f n a).
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f (int_succ n) a = f (int_iter f n a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f (int_succ n) a = f (int_iter f n a)
  destruct n as [n| |n]; trivial.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
int_iter f (int_succ (neg n)) a =
f (int_iter f (neg n) a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
int_iter f (int_succ (pos n)) a =
f (int_iter f (pos n) a)
  +
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
int_iter f (int_succ (neg n)) a =
f (int_iter f (neg n) a) revert n f H a.
A: Type
forall (n : Pos) (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
f (int_iter f (neg n) a)
    srapply pos_peano_ind.
A: Type
(fun p : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 int_iter f (int_succ (neg p)) a =
 f (int_iter f (neg p) a)) 1%pos
A: Type
forall p : Pos,
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 int_iter f (int_succ (neg p0)) a =
 f (int_iter f (neg p0) a)) p ->
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 int_iter f (int_succ (neg p0)) a =
 f (int_iter f (neg p0) a)) (pos_succ p)
    {
A: Type
(fun p : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 int_iter f (int_succ (neg p)) a =
 f (int_iter f (neg p) a)) 1%pos intros f H a.
A: Type
f: A -> A
H: IsEquiv f
a: A
int_iter f (int_succ (-1)%int) a =
f (int_iter f (-1)%int a)
      symmetry.
A: Type
f: A -> A
H: IsEquiv f
a: A
f (int_iter f (-1)%int a) =
int_iter f (int_succ (-1)%int) a
      apply eisretr. }
A: Type
forall p : Pos,
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 int_iter f (int_succ (neg p0)) a =
 f (int_iter f (neg p0) a)) p ->
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 int_iter f (int_succ (neg p0)) a =
 f (int_iter f (neg p0) a)) (pos_succ p)
    hnf; intros n p f H a.
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
f (int_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
int_iter f (int_succ (neg (pos_succ n))) a =
f (int_iter f (neg (pos_succ n)) a)
    refine (ap (fun x => _ x _) _ @ _).
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
f (int_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
int_succ (neg (pos_succ n)) = ?Goal0
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
f (int_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
int_iter f ?Goal0 a =
f (int_iter f (neg (pos_succ n)) a)
    1: rewrite int_neg_pos_succ.
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
f (int_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
int_succ (int_pred (neg n)) = ?Goal0
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
f (int_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
int_iter f ?Goal0 a =
f (int_iter f (neg (pos_succ n)) a)
    1: exact (eisretr int_succ (neg n)).
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
f (int_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
int_iter f (neg n) a =
f (int_iter f (neg (pos_succ n)) a)
    apply moveL_equiv_M.
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
f (int_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
f^-1 (int_iter f (neg n) a) =
int_iter f (neg (pos_succ n)) a
    cbn; symmetry.
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
f (int_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
pos_iter f^-1 (pos_succ n) a =
f^-1 (pos_iter f^-1 n a)
    srapply pos_iter_succ_l.
  +
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
int_iter f (int_succ (pos n)) a =
f (int_iter f (pos n) a) cbn.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
pos_iter f (n + 1)%pos a = f (pos_iter f n a)
    rewrite pos_add_1_r.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
pos_iter f (pos_succ n) a = f (pos_iter f n a)
    srapply pos_iter_succ_l.
Qed.

Definition int_iter_succ_r {A} (f : A -> A) `{IsEquiv _ _ f}
  (n : Int) (a : A) : int_iter f (int_succ n) a = int_iter f n (f a).
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f (int_succ n) a = int_iter f n (f a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f (int_succ n) a = int_iter f n (f a)
   destruct n as [n| |n]; trivial.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
int_iter f (int_succ (neg n)) a =
int_iter f (neg n) (f a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
int_iter f (int_succ (pos n)) a =
int_iter f (pos n) (f a)
+
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
int_iter f (int_succ (neg n)) a =
int_iter f (neg n) (f a) revert n f H a.
A: Type
forall (n : Pos) (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
int_iter f (neg n) (f a)
  srapply pos_peano_ind.
A: Type
(fun p : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 int_iter f (int_succ (neg p)) a =
 int_iter f (neg p) (f a)) 1%pos
A: Type
forall p : Pos,
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 int_iter f (int_succ (neg p0)) a =
 int_iter f (neg p0) (f a)) p ->
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 int_iter f (int_succ (neg p0)) a =
 int_iter f (neg p0) (f a)) (pos_succ p)
  {
A: Type
(fun p : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 int_iter f (int_succ (neg p)) a =
 int_iter f (neg p) (f a)) 1%pos intros f H a.
A: Type
f: A -> A
H: IsEquiv f
a: A
int_iter f (int_succ (-1)%int) a =
int_iter f (-1)%int (f a)
    symmetry.
A: Type
f: A -> A
H: IsEquiv f
a: A
int_iter f (-1)%int (f a) =
int_iter f (int_succ (-1)%int) a
    apply eissect. }
A: Type
forall p : Pos,
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 int_iter f (int_succ (neg p0)) a =
 int_iter f (neg p0) (f a)) p ->
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 int_iter f (int_succ (neg p0)) a =
 int_iter f (neg p0) (f a)) (pos_succ p)
  hnf; intros n p f H a.
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
int_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
int_iter f (int_succ (neg (pos_succ n))) a =
int_iter f (neg (pos_succ n)) (f a)
  rewrite int_neg_pos_succ.
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
int_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
int_iter f (int_succ (int_pred (neg n))) a =
int_iter f (int_pred (neg n)) (f a)
  refine (ap (fun x => _ x _) _ @ _).
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
int_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
int_succ (int_pred (neg n)) = ?Goal0
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
int_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
int_iter f ?Goal0 a =
int_iter f (int_pred (neg n)) (f a)
  1: exact (eisretr int_succ (neg n)).
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
int_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
int_iter f (neg n) a =
int_iter f (int_pred (neg n)) (f a)
  cbn; rewrite pos_add_1_r.
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
int_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
pos_iter f^-1 n a = pos_iter f^-1 (pos_succ n) (f a)
  rewrite pos_iter_succ_r.
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
int_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
pos_iter f^-1 n a = pos_iter f^-1 n (f^-1 (f a))
  rewrite eissect.
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
int_iter f (int_succ (neg n)) a =
int_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
pos_iter f^-1 n a = pos_iter f^-1 n a
  reflexivity.
+
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
int_iter f (int_succ (pos n)) a =
int_iter f (pos n) (f a) cbn.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
pos_iter f (n + 1)%pos a = pos_iter f n (f a)
  rewrite pos_add_1_r.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
pos_iter f (pos_succ n) a = pos_iter f n (f a)
  srapply pos_iter_succ_r.
Qed.

Definition iter_int_pred_l {A} (f : A -> A) `{IsEquiv _ _ f}
  (n : Int) (a : A)
: int_iter f (int_pred n) a = f^-1 (int_iter f n a).
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f (int_pred n) a = f^-1 (int_iter f n a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f (int_pred n) a = f^-1 (int_iter f n a)
  destruct n as [n| |n]; trivial.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
int_iter f (int_pred (neg n)) a =
f^-1 (int_iter f (neg n) a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
int_iter f (int_pred (pos n)) a =
f^-1 (int_iter f (pos n) a)
  +
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
int_iter f (int_pred (neg n)) a =
f^-1 (int_iter f (neg n) a) cbn; rewrite pos_add_1_r.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
pos_iter f^-1 (pos_succ n) a =
f^-1 (pos_iter f^-1 n a)
    by rewrite pos_iter_succ_l.
  +
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
int_iter f (int_pred (pos n)) a =
f^-1 (int_iter f (pos n) a) revert n.
A: Type
f: A -> A
H: IsEquiv f
a: A
forall n : Pos,
int_iter f (int_pred (pos n)) a =
f^-1 (int_iter f (pos n) a)
    srapply pos_peano_ind.
A: Type
f: A -> A
H: IsEquiv f
a: A
(fun p : Pos =>
 int_iter f (int_pred (pos p)) a =
 f^-1 (int_iter f (pos p) a)) 1%pos
A: Type
f: A -> A
H: IsEquiv f
a: A
forall p : Pos,
(fun p0 : Pos =>
 int_iter f (int_pred (pos p0)) a =
 f^-1 (int_iter f (pos p0) a)) p ->
(fun p0 : Pos =>
 int_iter f (int_pred (pos p0)) a =
 f^-1 (int_iter f (pos p0) a)) (pos_succ p)
    -
A: Type
f: A -> A
H: IsEquiv f
a: A
(fun p : Pos =>
 int_iter f (int_pred (pos p)) a =
 f^-1 (int_iter f (pos p) a)) 1%pos cbn; symmetry; apply eissect.
    -
A: Type
f: A -> A
H: IsEquiv f
a: A
forall p : Pos,
(fun p0 : Pos =>
 int_iter f (int_pred (pos p0)) a =
 f^-1 (int_iter f (pos p0) a)) p ->
(fun p0 : Pos =>
 int_iter f (int_pred (pos p0)) a =
 f^-1 (int_iter f (pos p0) a)) (pos_succ p) hnf; intros p q.
A: Type
f: A -> A
H: IsEquiv f
a: A
p: Pos
q: int_iter f (int_pred (pos p)) a =
f^-1 (int_iter f (pos p) a)
int_iter f (int_pred (pos (pos_succ p))) a =
f^-1 (int_iter f (pos (pos_succ p)) a)
      rewrite <- pos_add_1_r.
A: Type
f: A -> A
H: IsEquiv f
a: A
p: Pos
q: int_iter f (int_pred (pos p)) a =
f^-1 (int_iter f (pos p) a)
int_iter f (int_pred (pos (p + 1%pos))) a =
f^-1 (int_iter f (pos (p + 1%pos)) a)
      change (int_pred (pos (p + 1)%pos))
        with (int_pred (int_succ (pos p))).
A: Type
f: A -> A
H: IsEquiv f
a: A
p: Pos
q: int_iter f (int_pred (pos p)) a =
f^-1 (int_iter f (pos p) a)
int_iter f (int_pred (int_succ (pos p))) a =
f^-1 (int_iter f (pos (p + 1%pos)) a)
      rewrite int_pred_succ.
A: Type
f: A -> A
H: IsEquiv f
a: A
p: Pos
q: int_iter f (int_pred (pos p)) a =
f^-1 (int_iter f (pos p) a)
int_iter f (pos p) a =
f^-1 (int_iter f (pos (p + 1%pos)) a)
      change (pos (p + 1)%pos)
        with (int_succ (pos p)).
A: Type
f: A -> A
H: IsEquiv f
a: A
p: Pos
q: int_iter f (int_pred (pos p)) a =
f^-1 (int_iter f (pos p) a)
int_iter f (pos p) a =
f^-1 (int_iter f (int_succ (pos p)) a)
      rewrite int_iter_succ_l.
A: Type
f: A -> A
H: IsEquiv f
a: A
p: Pos
q: int_iter f (int_pred (pos p)) a =
f^-1 (int_iter f (pos p) a)
int_iter f (pos p) a = f^-1 (f (int_iter f (pos p) a))
      symmetry.
A: Type
f: A -> A
H: IsEquiv f
a: A
p: Pos
q: int_iter f (int_pred (pos p)) a =
f^-1 (int_iter f (pos p) a)
f^-1 (f (int_iter f (pos p) a)) = int_iter f (pos p) a
      apply eissect.
Qed.

Definition iter_int_pred_r {A} (f : A -> A) `{IsEquiv _ _ f}
  (n : Int) (a : A)
: int_iter f (int_pred n) a = int_iter f n (f^-1 a).
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f (int_pred n) a = int_iter f n (f^-1 a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f (int_pred n) a = int_iter f n (f^-1 a)
  revert f H n a.
A: Type
forall (f : A -> A) (H : IsEquiv f) (n : Int) (a : A),
int_iter f (int_pred n) a = int_iter f n (f^-1 a)
  destruct n as [n| |n]; trivial;
  induction n as [|n nH] using pos_peano_ind; trivial.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (neg n)) a =
int_iter f (neg n) (f^-1 a)
forall a : A,
int_iter f (int_pred (neg (pos_succ n))) a =
int_iter f (neg (pos_succ n)) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
forall a : A,
int_iter f (int_pred 1%int) a =
int_iter f 1%int (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (pos n)) a =
int_iter f (pos n) (f^-1 a)
forall a : A,
int_iter f (int_pred (pos (pos_succ n))) a =
int_iter f (pos (pos_succ n)) (f^-1 a)
  2: hnf; intros; apply symmetry, eisretr.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (neg n)) a =
int_iter f (neg n) (f^-1 a)
forall a : A,
int_iter f (int_pred (neg (pos_succ n))) a =
int_iter f (neg (pos_succ n)) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (pos n)) a =
int_iter f (pos n) (f^-1 a)
forall a : A,
int_iter f (int_pred (pos (pos_succ n))) a =
int_iter f (pos (pos_succ n)) (f^-1 a)
  all: rewrite <- pos_add_1_r.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (neg n)) a =
int_iter f (neg n) (f^-1 a)
forall a : A,
int_iter f (int_pred (neg (n + 1)%pos)) a =
int_iter f (neg (n + 1)%pos) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (pos n)) a =
int_iter f (pos n) (f^-1 a)
forall a : A,
int_iter f (int_pred (pos (n + 1%pos))) a =
int_iter f (pos (n + 1%pos)) (f^-1 a)
  all: intro a.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (neg n)) a =
int_iter f (neg n) (f^-1 a)
a: A
int_iter f (int_pred (neg (n + 1)%pos)) a =
int_iter f (neg (n + 1)%pos) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (pos n)) a =
int_iter f (pos n) (f^-1 a)
a: A
int_iter f (int_pred (pos (n + 1%pos))) a =
int_iter f (pos (n + 1%pos)) (f^-1 a)
  1: change (neg (n + 1)%pos) with (int_pred (neg n)).
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (neg n)) a =
int_iter f (neg n) (f^-1 a)
a: A
int_iter f (int_pred (int_pred (neg n))) a =
int_iter f (int_pred (neg n)) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (pos n)) a =
int_iter f (pos n) (f^-1 a)
a: A
int_iter f (int_pred (pos (n + 1%pos))) a =
int_iter f (pos (n + 1%pos)) (f^-1 a)
  2: change (pos (n + 1)%pos) with (int_succ (pos n)).
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (neg n)) a =
int_iter f (neg n) (f^-1 a)
a: A
int_iter f (int_pred (int_pred (neg n))) a =
int_iter f (int_pred (neg n)) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (pos n)) a =
int_iter f (pos n) (f^-1 a)
a: A
int_iter f (int_pred (int_succ (pos n))) a =
int_iter f (int_succ (pos n)) (f^-1 a)
  1: rewrite <- 2 int_neg_pos_succ.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (neg n)) a =
int_iter f (neg n) (f^-1 a)
a: A
int_iter f (neg (pos_succ (pos_succ n))) a =
int_iter f (neg (pos_succ n)) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (pos n)) a =
int_iter f (pos n) (f^-1 a)
a: A
int_iter f (int_pred (int_succ (pos n))) a =
int_iter f (int_succ (pos n)) (f^-1 a)
  1: cbn; apply pos_iter_succ_r.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (pos n)) a =
int_iter f (pos n) (f^-1 a)
a: A
int_iter f (int_pred (int_succ (pos n))) a =
int_iter f (int_succ (pos n)) (f^-1 a)
  rewrite int_pred_succ.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (pos n)) a =
int_iter f (pos n) (f^-1 a)
a: A
int_iter f (pos n) a =
int_iter f (int_succ (pos n)) (f^-1 a)
  rewrite int_iter_succ_r.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (pos n)) a =
int_iter f (pos n) (f^-1 a)
a: A
int_iter f (pos n) a = int_iter f (pos n) (f (f^-1 a))
  rewrite eisretr.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
int_iter f (int_pred (pos n)) a =
int_iter f (pos n) (f^-1 a)
a: A
int_iter f (pos n) a = int_iter f (pos n) a
  reflexivity.
Qed.