proposition: Lemma Clt_le_weak : forall i j : nat, Clt i j -> Cle i j.
proof: Proof. intros. apply toCle; apply Nat.lt_le_incl; apply Clt_to; assumption. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)