proposition: Lemma expR_lt1 x : (expR x < 1) = (x < 0).
proof: Proof. case: ltrgt0P => [x_gt0|xN|->]; last by rewrite expR0. - by apply/idP/negP; rewrite -leNgt ltW // expR_gt1. - by rewrite -[x]opprK expRN invf_cp1 ?expR_gt0 // expR_gt1 lterNE. 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