proposition: Lemma ler_expR : {mono (@expR R) : x y / x <= y}.
proof: Proof. move=> x y. case: (ltrgtP x y) => [xLy|yLx|<-]; last by rewrite lexx. - by rewrite ltW // ltr_expR. - by rewrite leNgt ltr_expR yLx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex