proposition: Lemma compare_opp n m : (- n ?= - m) = (m ?= n).
proof: Proof. destruct n, m; simpl; trivial; intros; now rewrite <- Pos.compare_antisym. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass