a b : - (binint_pos_sub a b) = binint_pos_sub b a. Proof. revert a b. induction a as [|a ah|a ah]; destruct b; cbn; trivial. all: rewrite ?binint_negation_double, ?binint_negation_succ_double, ?binint_negation_pred_double. all: apply ap, ah. Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.