proposition: Lemma poweRD x r s : x `^?(r +? s) -> x `^ (r + s) = x `^ r * x `^ s.
proof: Proof. rewrite /poweRD_def. have [->|r0]/= := eqVneq r 0%R; first by rewrite add0r poweRe0 mul1e. have [->|s0]/= := eqVneq s 0%R; first by rewrite addr0 poweRe0 mule1. case: x => // [t|/=|/=]; rewrite ?(negPf r0, negPf s0, implybF); last 2 first. - by move=> /negPf->; rewrite mulyy. - by move=> /negPf->; rewrite mule0. rewrite !poweR_EFin eqe => /implyP/(_ _)/andP cnd. by rewrite powRD//; apply/implyP => /cnd[]. 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