{A} (f : A -> A) `{IsEquiv _ _ f} (n : BinInt) (a : A) : binint_iter f (binint_pred n) a = binint_iter f n (f^-1 a). Proof. revert f H n a. destruct n as [n| |n]; trivial; induction n as [|n nH] using pos_peano_ind; trivial. 2: hnf; intros; apply symmetry, eisretr. all: rewrite <- pos_add_1_r. all: intro a. 1: change (neg (n + 1)%pos) with (binint_pred (neg n)). 2: change (pos (n + 1)%pos) with (binint_succ (pos n)). 1: rewrite <- 2 binint_neg_pos_succ. 1: cbn; apply pos_iter_succ_r. rewrite binint_pred_succ. rewrite binint_iter_succ_r. rewrite eisretr. reflexivity. Qed.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core. Require Import Spaces.BinInt.Spec.