proposition: Theorem compare_antisym n m : (m ?= n) = CompOpp (n ?= m).
proof: Proof. destruct n, m; simpl; trivial. apply Pos.compare_antisym. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties