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