proposition: Lemma T1log_exp1 z x: T1nf z -> T1nf x -> ~~ T1finite z -> T1log (z ^ x) = (T1log z) * x.
proof: Proof. move => nz nx. case zz: (z== zero); first by rewrite (eqP zz). move: (nf_rev nx); rewrite /T1exp. set u := T1div_by_omega (T1split x).1; set n := (T1split x).2. move => [nu ->]; rewrite T1log_prod ?expO_eq0 ? expF_eq0 ? zz //. rewrite T1log_exp0 // mul_distr mulA => h; congr T1add. rewrite /exp_O zz (negbTE h) fun_if /phi0 ifF //. move: h; case z => // a m b /=; case a => //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)