proposition: Lemma le_1 : forall m n : nat, Cle m n -> pred m <= n.
proof: Proof. intros. cut (m <= n); [ intro | apply Cle_to; assumption ]. apply Nat.le_trans with (pred n); auto with arith. apply Nat.pred_le_mono; auto. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)