{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.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core. Require Import Spaces.BinInt.Spec.