proposition: Lemma power_strext : forall x x' y y' Hx Hx', x[!]y[//]Hx [#] x'[!]y'[//]Hx' -> x [#] x' or y [#] y'.
proof: Proof. intros. cut (Log x Hx [#] Log x' Hx' or y [#] y'). intro H0. elim H0; intro H1; [ left | right ]; auto; exact (Log_strext _ _ _ _ H1). apply bin_op_strext_unfolded with (cr_mult (c:=IR)). astepl (y[*]Log x Hx); astepr (y'[*]Log x' Hx'). apply Exp_strext; auto. Qed.
imports: CoRN.transc.Exponential