a b : binint_pred a + b = binint_pred (a + b). Proof. rewrite <- binint_add_assoc, (binint_add_comm (-1) b). apply binint_add_assoc. Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.