a b : binint_succ a + b = binint_succ (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.