proposition: Lemma real_power_resp_leEq_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_leEq. apply mult_resp_leEq_lft; try assumption. apply Log_resp_leEq. assumption. Qed.
imports: CoRN.transc.Exponential