proposition: Theorem nat_compare_dec: forall m n, (n < m [+] m <= n ).
proof: Proof. induction m. destruct n. right. auto. right. omega. intros. destruct (IHm n); destruct (eq_nat_dec n m); subst; try( left; omega); try( right; omega). Qed.
imports: UsefulTypes bin_rels Omega