proposition: Lemma real_power_resp_leEq_both : forall x y p q Hx Hy', [1][<=]x -> [0] [<=] p -> x[<=]y -> p[<=]q -> x[!]p[//]Hx [<=] y[!]q[//]Hy'.
proof: Proof. intros x y p q Hx Hy Hx0 Hp H0 H1. apply leEq_transitive with (y[!]p[//]Hy). apply real_power_resp_leEq_rht; assumption. apply real_power_resp_leEq_lft; try assumption. apply leEq_transitive with x; assumption. Qed.
imports: CoRN.transc.Exponential