proposition: Lemma k_zero:forall (k i l:nat), Not (0<k or 0=k and i<l)-> k=0.
proof: Proof. intros k i l H. unfold Not in H. set (H1:=(lt_eq_lt_dec 0 k)). elim H1. clear H1. intro H1. elim H1. clear H1. intuition. intuition. intuition. Qed.
imports: Coq.Arith.Peano_dec Coq.Relations.Relations CoRN.logic.CLogic Coq(Lia)