proposition: Lemma div_power : forall x y z Hx Hy Hy' Hxy Hyz, (x[/] y[//]Hy') [!]z[//]Hxy [=] (x[!]z[//]Hx[/] y[!]z[//]Hy[//]Hyz).
proof: Proof. intros. apply eq_transitive_unfolded with ((x[*] ([1][/] _[//]Hy')) [!]z[//] mult_resp_pos _ _ _ Hx (recip_resp_pos _ _ Hy' Hy)). apply power_wd; rational. rstepr (x[!]z[//]Hx[*] ([1][/] _[//]Hyz)). Step_final (x[!]z[//]Hx[*]_[!]z[//]recip_resp_pos _ _ Hy' Hy). Qed.
imports: CoRN.transc.Exponential