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

(** ** Iteration of equivalences *)

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

Definition binint_iter {A} (f : A -> A) `{!IsEquiv f} (n : BinInt) : 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 binint_iter_succ_l {A} (f : A -> A) `{IsEquiv _ _ f}
  (n : BinInt) (a : A)
  : binint_iter f (binint_succ n) a = f (binint_iter f n a).
A: Type
f: A -> A
H: IsEquiv f
n: BinInt
a: A
binint_iter f (binint_succ n) a =
f (binint_iter f n a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: BinInt
a: A
binint_iter f (binint_succ n) a =
f (binint_iter f n a)
  destruct n as [n| |n]; trivial.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
binint_iter f (binint_succ (neg n)) a =
f (binint_iter f (neg n) a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
binint_iter f (binint_succ (pos n)) a =
f (binint_iter f (pos n) a)
  +
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
binint_iter f (binint_succ (neg n)) a =
f (binint_iter f (neg n) a) revert n f H a.
A: Type
forall (n : Pos) (f : A -> A) (H : IsEquiv f) (a : A),
binint_iter f (binint_succ (neg n)) a =
f (binint_iter f (neg n) a)
    srapply pos_peano_ind.
A: Type
(fun p : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 binint_iter f (binint_succ (neg p)) a =
 f (binint_iter f (neg p) a)) 1%pos
A: Type
forall p : Pos,
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 binint_iter f (binint_succ (neg p0)) a =
 f (binint_iter f (neg p0) a)) p ->
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 binint_iter f (binint_succ (neg p0)) a =
 f (binint_iter f (neg p0) a)) (pos_succ p)
    {
A: Type
(fun p : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 binint_iter f (binint_succ (neg p)) a =
 f (binint_iter f (neg p) a)) 1%pos intros f H a.
A: Type
f: A -> A
H: IsEquiv f
a: A
binint_iter f (binint_succ (-1)%binint) a =
f (binint_iter f (-1)%binint a)
      symmetry.
A: Type
f: A -> A
H: IsEquiv f
a: A
f (binint_iter f (-1)%binint a) =
binint_iter f (binint_succ (-1)%binint) a
      apply eisretr. }
A: Type
forall p : Pos,
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 binint_iter f (binint_succ (neg p0)) a =
 f (binint_iter f (neg p0) a)) p ->
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 binint_iter f (binint_succ (neg p0)) a =
 f (binint_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),
binint_iter f (binint_succ (neg n)) a =
f (binint_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
binint_iter f (binint_succ (neg (pos_succ n))) a =
f (binint_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),
binint_iter f (binint_succ (neg n)) a =
f (binint_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
binint_succ (neg (pos_succ n)) = ?Goal0
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
binint_iter f (binint_succ (neg n)) a =
f (binint_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
binint_iter f ?Goal0 a =
f (binint_iter f (neg (pos_succ n)) a)
    1: rewrite binint_neg_pos_succ.
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
binint_iter f (binint_succ (neg n)) a =
f (binint_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
binint_succ (binint_pred (neg n)) = ?Goal0
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
binint_iter f (binint_succ (neg n)) a =
f (binint_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
binint_iter f ?Goal0 a =
f (binint_iter f (neg (pos_succ n)) a)
    1: exact (eisretr binint_succ (neg n)).
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
binint_iter f (binint_succ (neg n)) a =
f (binint_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
binint_iter f (neg n) a =
f (binint_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),
binint_iter f (binint_succ (neg n)) a =
f (binint_iter f (neg n) a)
f: A -> A
H: IsEquiv f
a: A
f^-1 (binint_iter f (neg n) a) =
binint_iter f (neg (pos_succ n)) a
    cbn; symmetry.
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
binint_iter f (binint_succ (neg n)) a =
f (binint_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
binint_iter f (binint_succ (pos n)) a =
f (binint_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 binint_iter_succ_r {A} (f : A -> A) `{IsEquiv _ _ f}
  (n : BinInt) (a : A) : binint_iter f (binint_succ n) a = binint_iter f n (f a).
A: Type
f: A -> A
H: IsEquiv f
n: BinInt
a: A
binint_iter f (binint_succ n) a =
binint_iter f n (f a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: BinInt
a: A
binint_iter f (binint_succ n) a =
binint_iter f n (f a)
   destruct n as [n| |n]; trivial.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
binint_iter f (binint_succ (neg n)) a =
binint_iter f (neg n) (f a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
binint_iter f (binint_succ (pos n)) a =
binint_iter f (pos n) (f a)
+
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
binint_iter f (binint_succ (neg n)) a =
binint_iter f (neg n) (f a) revert n f H a.
A: Type
forall (n : Pos) (f : A -> A) (H : IsEquiv f) (a : A),
binint_iter f (binint_succ (neg n)) a =
binint_iter f (neg n) (f a)
  srapply pos_peano_ind.
A: Type
(fun p : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 binint_iter f (binint_succ (neg p)) a =
 binint_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),
 binint_iter f (binint_succ (neg p0)) a =
 binint_iter f (neg p0) (f a)) p ->
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 binint_iter f (binint_succ (neg p0)) a =
 binint_iter f (neg p0) (f a)) (pos_succ p)
  {
A: Type
(fun p : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 binint_iter f (binint_succ (neg p)) a =
 binint_iter f (neg p) (f a)) 1%pos intros f H a.
A: Type
f: A -> A
H: IsEquiv f
a: A
binint_iter f (binint_succ (-1)%binint) a =
binint_iter f (-1)%binint (f a)
    symmetry.
A: Type
f: A -> A
H: IsEquiv f
a: A
binint_iter f (-1)%binint (f a) =
binint_iter f (binint_succ (-1)%binint) a
    apply eissect. }
A: Type
forall p : Pos,
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 binint_iter f (binint_succ (neg p0)) a =
 binint_iter f (neg p0) (f a)) p ->
(fun p0 : Pos =>
 forall (f : A -> A) (H : IsEquiv f) (a : A),
 binint_iter f (binint_succ (neg p0)) a =
 binint_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),
binint_iter f (binint_succ (neg n)) a =
binint_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
binint_iter f (binint_succ (neg (pos_succ n))) a =
binint_iter f (neg (pos_succ n)) (f a)
  rewrite binint_neg_pos_succ.
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
binint_iter f (binint_succ (neg n)) a =
binint_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
binint_iter f (binint_succ (binint_pred (neg n))) a =
binint_iter f (binint_pred (neg n)) (f a)
  refine (ap (fun x => _ x _) _ @ _).
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
binint_iter f (binint_succ (neg n)) a =
binint_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
binint_succ (binint_pred (neg n)) = ?Goal0
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
binint_iter f (binint_succ (neg n)) a =
binint_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
binint_iter f ?Goal0 a =
binint_iter f (binint_pred (neg n)) (f a)
  1: exact (eisretr binint_succ (neg n)).
A: Type
n: Pos
p: forall (f : A -> A) (H : IsEquiv f) (a : A),
binint_iter f (binint_succ (neg n)) a =
binint_iter f (neg n) (f a)
f: A -> A
H: IsEquiv f
a: A
binint_iter f (neg n) a =
binint_iter f (binint_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),
binint_iter f (binint_succ (neg n)) a =
binint_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),
binint_iter f (binint_succ (neg n)) a =
binint_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),
binint_iter f (binint_succ (neg n)) a =
binint_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
binint_iter f (binint_succ (pos n)) a =
binint_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_binint_pred_l {A} (f : A -> A) `{IsEquiv _ _ f}
  (n : BinInt) (a : A)
: binint_iter f (binint_pred n) a = f^-1 (binint_iter f n a).
A: Type
f: A -> A
H: IsEquiv f
n: BinInt
a: A
binint_iter f (binint_pred n) a =
f^-1 (binint_iter f n a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: BinInt
a: A
binint_iter f (binint_pred n) a =
f^-1 (binint_iter f n a)
  destruct n as [n| |n]; trivial.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
binint_iter f (binint_pred (neg n)) a =
f^-1 (binint_iter f (neg n) a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
binint_iter f (binint_pred (pos n)) a =
f^-1 (binint_iter f (pos n) a)
  +
A: Type
f: A -> A
H: IsEquiv f
n: Pos
a: A
binint_iter f (binint_pred (neg n)) a =
f^-1 (binint_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
binint_iter f (binint_pred (pos n)) a =
f^-1 (binint_iter f (pos n) a) revert n.
A: Type
f: A -> A
H: IsEquiv f
a: A
forall n : Pos,
binint_iter f (binint_pred (pos n)) a =
f^-1 (binint_iter f (pos n) a)
    srapply pos_peano_ind.
A: Type
f: A -> A
H: IsEquiv f
a: A
(fun p : Pos =>
 binint_iter f (binint_pred (pos p)) a =
 f^-1 (binint_iter f (pos p) a)) 1%pos
A: Type
f: A -> A
H: IsEquiv f
a: A
forall p : Pos,
(fun p0 : Pos =>
 binint_iter f (binint_pred (pos p0)) a =
 f^-1 (binint_iter f (pos p0) a)) p ->
(fun p0 : Pos =>
 binint_iter f (binint_pred (pos p0)) a =
 f^-1 (binint_iter f (pos p0) a)) (pos_succ p)
    -
A: Type
f: A -> A
H: IsEquiv f
a: A
(fun p : Pos =>
 binint_iter f (binint_pred (pos p)) a =
 f^-1 (binint_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 =>
 binint_iter f (binint_pred (pos p0)) a =
 f^-1 (binint_iter f (pos p0) a)) p ->
(fun p0 : Pos =>
 binint_iter f (binint_pred (pos p0)) a =
 f^-1 (binint_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: binint_iter f (binint_pred (pos p)) a =
f^-1 (binint_iter f (pos p) a)
binint_iter f (binint_pred (pos (pos_succ p))) a =
f^-1 (binint_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: binint_iter f (binint_pred (pos p)) a =
f^-1 (binint_iter f (pos p) a)
binint_iter f (binint_pred (pos (p + 1%pos))) a =
f^-1 (binint_iter f (pos (p + 1%pos)) a)
      change (binint_pred (pos (p + 1)%pos))
        with (binint_pred (binint_succ (pos p))).
A: Type
f: A -> A
H: IsEquiv f
a: A
p: Pos
q: binint_iter f (binint_pred (pos p)) a =
f^-1 (binint_iter f (pos p) a)
binint_iter f (binint_pred (binint_succ (pos p))) a =
f^-1 (binint_iter f (pos (p + 1%pos)) a)
      rewrite binint_pred_succ.
A: Type
f: A -> A
H: IsEquiv f
a: A
p: Pos
q: binint_iter f (binint_pred (pos p)) a =
f^-1 (binint_iter f (pos p) a)
binint_iter f (pos p) a =
f^-1 (binint_iter f (pos (p + 1%pos)) a)
      change (pos (p + 1)%pos)
        with (binint_succ (pos p)).
A: Type
f: A -> A
H: IsEquiv f
a: A
p: Pos
q: binint_iter f (binint_pred (pos p)) a =
f^-1 (binint_iter f (pos p) a)
binint_iter f (pos p) a =
f^-1 (binint_iter f (binint_succ (pos p)) a)
      rewrite binint_iter_succ_l.
A: Type
f: A -> A
H: IsEquiv f
a: A
p: Pos
q: binint_iter f (binint_pred (pos p)) a =
f^-1 (binint_iter f (pos p) a)
binint_iter f (pos p) a =
f^-1 (f (binint_iter f (pos p) a))
      symmetry.
A: Type
f: A -> A
H: IsEquiv f
a: A
p: Pos
q: binint_iter f (binint_pred (pos p)) a =
f^-1 (binint_iter f (pos p) a)
f^-1 (f (binint_iter f (pos p) a)) =
binint_iter f (pos p) a
      apply eissect.
Qed.

Definition iter_binint_pred_r {A} (f : A -> A) `{IsEquiv _ _ f}
  (n : BinInt) (a : A)
: binint_iter f (binint_pred n) a = binint_iter f n (f^-1 a).
A: Type
f: A -> A
H: IsEquiv f
n: BinInt
a: A
binint_iter f (binint_pred n) a =
binint_iter f n (f^-1 a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: BinInt
a: A
binint_iter f (binint_pred n) a =
binint_iter f n (f^-1 a)
  revert f H n a.
A: Type
forall (f : A -> A) (H : IsEquiv f) (n : BinInt)
(a : A),
binint_iter f (binint_pred n) a =
binint_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,
binint_iter f (binint_pred (neg n)) a =
binint_iter f (neg n) (f^-1 a)
forall a : A,
binint_iter f (binint_pred (neg (pos_succ n))) a =
binint_iter f (neg (pos_succ n)) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
forall a : A,
binint_iter f (binint_pred 1%binint) a =
binint_iter f 1%binint (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (pos n)) a =
binint_iter f (pos n) (f^-1 a)
forall a : A,
binint_iter f (binint_pred (pos (pos_succ n))) a =
binint_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,
binint_iter f (binint_pred (neg n)) a =
binint_iter f (neg n) (f^-1 a)
forall a : A,
binint_iter f (binint_pred (neg (pos_succ n))) a =
binint_iter f (neg (pos_succ n)) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (pos n)) a =
binint_iter f (pos n) (f^-1 a)
forall a : A,
binint_iter f (binint_pred (pos (pos_succ n))) a =
binint_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,
binint_iter f (binint_pred (neg n)) a =
binint_iter f (neg n) (f^-1 a)
forall a : A,
binint_iter f (binint_pred (neg (n + 1)%pos)) a =
binint_iter f (neg (n + 1)%pos) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (pos n)) a =
binint_iter f (pos n) (f^-1 a)
forall a : A,
binint_iter f (binint_pred (pos (n + 1%pos))) a =
binint_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,
binint_iter f (binint_pred (neg n)) a =
binint_iter f (neg n) (f^-1 a)
a: A
binint_iter f (binint_pred (neg (n + 1)%pos)) a =
binint_iter f (neg (n + 1)%pos) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (pos n)) a =
binint_iter f (pos n) (f^-1 a)
a: A
binint_iter f (binint_pred (pos (n + 1%pos))) a =
binint_iter f (pos (n + 1%pos)) (f^-1 a)
  1: change (neg (n + 1)%pos) with (binint_pred (neg n)).
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (neg n)) a =
binint_iter f (neg n) (f^-1 a)
a: A
binint_iter f (binint_pred (binint_pred (neg n))) a =
binint_iter f (binint_pred (neg n)) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (pos n)) a =
binint_iter f (pos n) (f^-1 a)
a: A
binint_iter f (binint_pred (pos (n + 1%pos))) a =
binint_iter f (pos (n + 1%pos)) (f^-1 a)
  2: change (pos (n + 1)%pos) with (binint_succ (pos n)).
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (neg n)) a =
binint_iter f (neg n) (f^-1 a)
a: A
binint_iter f (binint_pred (binint_pred (neg n))) a =
binint_iter f (binint_pred (neg n)) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (pos n)) a =
binint_iter f (pos n) (f^-1 a)
a: A
binint_iter f (binint_pred (binint_succ (pos n))) a =
binint_iter f (binint_succ (pos n)) (f^-1 a)
  1: rewrite <- 2 binint_neg_pos_succ.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (neg n)) a =
binint_iter f (neg n) (f^-1 a)
a: A
binint_iter f (neg (pos_succ (pos_succ n))) a =
binint_iter f (neg (pos_succ n)) (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (pos n)) a =
binint_iter f (pos n) (f^-1 a)
a: A
binint_iter f (binint_pred (binint_succ (pos n))) a =
binint_iter f (binint_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,
binint_iter f (binint_pred (pos n)) a =
binint_iter f (pos n) (f^-1 a)
a: A
binint_iter f (binint_pred (binint_succ (pos n))) a =
binint_iter f (binint_succ (pos n)) (f^-1 a)
  rewrite binint_pred_succ.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (pos n)) a =
binint_iter f (pos n) (f^-1 a)
a: A
binint_iter f (pos n) a =
binint_iter f (binint_succ (pos n)) (f^-1 a)
  rewrite binint_iter_succ_r.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (pos n)) a =
binint_iter f (pos n) (f^-1 a)
a: A
binint_iter f (pos n) a =
binint_iter f (pos n) (f (f^-1 a))
  rewrite eisretr.
A: Type
f: A -> A
H: IsEquiv f
n: Pos
nH: forall a : A,
binint_iter f (binint_pred (pos n)) a =
binint_iter f (pos n) (f^-1 a)
a: A
binint_iter f (pos n) a = binint_iter f (pos n) a
  reflexivity.
Qed.