a : binint_pos_sub (pos_succ a) 1%pos = pos a. Proof. destruct a; trivial. cbn; apply ap, pos_pred_double_succ. Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.