proposition: Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
proof: Proof. destruct n, m; simpl; rewrite ?CompOpp_iff, ?Pos.compare_eq_iff; split; congruence. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass