n m p : n + (m + p) = n + m + p. Proof. destruct n. - apply binint_negation_inj. rewrite !binint_negation_add_distr. apply binint_add_assoc_pos. - trivial. - apply binint_add_assoc_pos. Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.