proposition: Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}.
proof: Proof. intro n; induction n as [|n IHn]; intro m; destruct m as [|m]. - now left. - now right. - now right. - destruct (IHn m); [left|right]; auto. Defined.
imports: NAxioms NProperties OrdersFacts DecidableClass