proposition: Lemma int_add_assoc n m p : n + (m + p) = n + m + p.
proof: Proof. destruct n. - apply int_negation_inj. rewrite !int_negation_add_distr. apply int_add_assoc_pos. - trivial. - apply int_add_assoc_pos. Defined.
imports: Basics Spaces.Pos Spaces.Int.Core