proposition: Lemma expeRD x y : expeR (x + y) = expeR x * expeR y.
proof: Proof. case: x => /= [r| |]; last by rewrite mul0e. - case: y => /= [s| |]; last by rewrite mule0. + by rewrite expRD EFinM. + by rewrite mulry gtr0_sg ?mul1e// expR_gt0. - case: y => /= [s| |]; last by rewrite mule0. + by rewrite mulyr gtr0_sg ?mul1e// expR_gt0. + by rewrite mulyy. 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