proposition: Lemma expRN x : expR (- x) = (expR x)^-1.
proof: Proof. apply: (mulfI (lt0r_neq0 (expR_gt0 x))). by rewrite expRxMexpNx_1 mulfV // (lt0r_neq0 (expR_gt0 x)). 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