proposition: Lemma Clt_to : forall m n : nat, Clt m n -> m < n.
proof: Proof. unfold lt in |- *. unfold Clt in |- *. intros m n H. apply Cle_to. assumption. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)