proposition: Lemma real_power_resp_leEq_lft : forall x p q Hx Hx', [1][<=]x -> p[<=]q -> x[!]p[//]Hx [<=] x[!]q[//]Hx'.
proof: Proof. intros x p q Hx Hx' Hx0 H. unfold power. apply Exp_resp_leEq. stepr (q[*]Log x Hx); [| now csetoid_rewrite (Log_wd x x Hx Hx' (eq_reflexive IR x)); apply eq_reflexive]. apply mult_resp_leEq_rht; try assumption. apply Zero_leEq_Log. assumption. Qed.
imports: CoRN.transc.Exponential