proposition: Lemma int_add_assoc_pos p n m : pos p + (n + m) = pos p + n + m.
proof: Proof. destruct n as [n| |n], m as [m| |m]; trivial. - cbn; apply int_negation_inj. rewrite !int_negation_add_distr, !int_pos_sub_negation. rewrite int_add_comm, pos_add_comm. apply int_pos_sub_add. - symmetry. apply int_add_0_r. - by rewrite <- int_pos_sub_add, int_add_comm, <- int_pos_sub_add, pos_add_comm. - symmetry. apply int_pos_sub_add. - cbn; apply ap, pos_add_assoc. Defined.
imports: Basics Spaces.Pos Spaces.Int.Core