proposition: Lemma lexi_dec:(forall (k i l:nat), Cdecidable (0<k or 0=k and i<l)):CProp.
proof: Proof. intros k i l. unfold Cdecidable. set (H:=(lt_eq_lt_dec 0 k)). elim H. clear H. intro H. elim H. clear H. intro H. left. left. exact H. clear H. intro H. elim (le_gt_dec l i). intro H1. right. unfold Not. intro H2. intuition. intro H1. left. right. intuition. intuition. Qed.
imports: Coq.Arith.Peano_dec Coq.Relations.Relations CoRN.logic.CLogic Coq(Lia)