proposition: Lemma toCle : forall m n : nat, m <= n -> Cle m n.
proof: Proof. intros m. induction m as [| m Hrecm]. simple induction n. intro H. apply Cle_n. intros n0 H H0. apply Cle_S. apply H. apply Nat.le_0_l. simple induction n. intro. exfalso. inversion H. intros n0 H H0. generalize (le_S_n _ _ H0); intro H1. generalize (Hrecm _ H1); intro H2. apply Cle_n_S. assumption. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)