{A} (f : A -> A) `{IsEquiv _ _ f} (n : BinInt) (a : A) : binint_iter f (binint_pred n) a = f^-1 (binint_iter f n a). Proof. destruct n as [n| |n]; trivial. + cbn; rewrite pos_add_1_r. by rewrite pos_iter_succ_l. + revert n. srapply pos_peano_ind. - cbn; symmetry; apply eissect. - hnf; intros p q. rewrite <- pos_add_1_r. change (binint_pred (pos (p + 1)%pos)) with (binint_pred (binint_succ (pos p))). rewrite binint_pred_succ. change (pos (p + 1)%pos) with (binint_succ (pos p)). rewrite binint_iter_succ_l. symmetry. apply eissect. Qed.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core. Require Import Spaces.BinInt.Spec.