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