proposition: Lemma real_power_resp_less_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 less_transitive_unfolded with (y[!]p[//]Hy). apply real_power_resp_less_rht; assumption. apply real_power_resp_less_lft; try assumption. apply less_transitive_unfolded with x; assumption. Qed.
imports: CoRN.transc.Exponential