proposition: Theorem compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
proof: Proof. destruct n, m; simpl; rewrite ?Pos.compare_eq_iff; split; congruence. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties