proposition: Lemma Cle_to : forall m n : nat, Cle m n -> m <= n.
proof: Proof. intros m n H. elim H. apply le_n. intros m0 s H0. apply le_S. assumption. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)