proposition: Theorem le_gt_cases : forall n m, n <= m \/ n > m.
proof: Proof. intros n m; nzinduct n m. - left; apply le_refl. - intro n. rewrite lt_succ_r, le_succ_l, !lt_eq_cases. intuition auto with relations. Qed.
imports: NZAxioms NZBase Decidable OrdersTac