n m : -n = -m -> n = m. 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.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.