proposition: Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
proof: Proof. revert m; induction n as [|n IHn]; intro m; destruct m; simpl; rewrite ?IHn; split; auto; easy. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass