proposition: Lemma expR_gt0 x : 0 < expR x.
proof: Proof. case: (ltrgt0P x) => [x_gt0|x_gt0|->]; last by rewrite expR0. - exact: lt_trans (pexpR_gt1 x_gt0). - have F : 0 < expR (- x) by rewrite (lt_trans _ (pexpR_gt1 _))// oppr_gt0. by rewrite -(pmulr_lgt0 _ F) expRxMexpNx_1. 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