proposition: Lemma Cnat_total_order : forall m n : nat, m <> n -> {m < n} + {n < m}.
proof: Proof. intros m n H. elim (gt_eq_gt_dec m n). intro H0. elim H0; intros. left; auto. exfalso. auto. auto. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)