proposition: Lemma ln_le x y : 0 < x -> x <= y -> ln x <= ln y.
proof: Proof. intros Hx Hxy ; destruct Hxy. left ; apply ln_increasing. exact Hx. exact H. rewrite H ; exact (Rle_refl _). Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)