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