proposition: Lemma real_power_resp_less_rht : forall x y p Hx Hy, [0][<] p -> x[<]y -> x[!]p[//]Hx [<] y[!]p[//]Hy.
proof: Proof. intros x y p Hp Hx Hy H. unfold power. apply Exp_resp_less. apply mult_resp_less_lft; try assumption. apply Log_resp_less. assumption. Qed.
imports: CoRN.transc.Exponential