proposition: Lemma int_negation_inj n m : -n = -m -> n = m.
proof: Proof. destruct n, m; simpl; intro H. 1: apply pos_inj in H. 2: apply pos_neq_zero in H. 3: apply pos_neq_neg in H. 4: apply zero_neq_pos in H. 6: apply zero_neq_neg in H. 7: apply neg_neq_pos in H. 8: apply neg_neq_zero in H. 9: apply neg_inj in H. all: by destruct H. Defined.
imports: Basics Spaces.Pos Spaces.Int.Core