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