p n m : pos p + (n + m) = pos p + n + m. Proof. destruct n as [n| |n], m as [m| |m]; trivial. - cbn; apply binint_negation_inj. rewrite !binint_negation_add_distr, !binint_pos_sub_negation. rewrite binint_add_comm, pos_add_comm. apply binint_pos_sub_add. - symmetry. apply binint_add_0_r. - by rewrite <- binint_pos_sub_add, binint_add_comm, <- binint_pos_sub_add, pos_add_comm. - symmetry. apply binint_pos_sub_add. - cbn; apply ap, pos_add_assoc. Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.