proposition: Lemma le_trans : forall l k n : nat, k <= l -> l <= n -> k <= n.
proof: Proof. intros l k n Hkl Hln. induction n as [| n Hrecn]. inversion Hln. rewrite <- H. exact Hkl. inversion Hln. rewrite <- H. exact Hkl. apply le_S. apply Hrecn. assumption. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)