proposition: Theorem eq_dne : forall n m, ~ ~ n == m <-> n == m.
proof: Proof. intros n m; split; intro H. - destruct (eq_decidable n m) as [H1 | H1]. + assumption. + false_hyp H1 H. - intro H1; now apply H1. Qed.
imports: NZAxioms NZBase Decidable OrdersTac