proposition: Lemma T1log_exp2 z u v: (z == zero) = false -> (z == one) = false -> T1finite z -> T1nf u -> T1log (z ^ (T1omega * u + \F v)) = u.
proof: Proof. move => z0 z1 fz nu; rewrite /T1exp. have aux: T1log (exp_F z v) = zero. elim v => // n h; rewrite T1log_prod -/exp_F ? z0 ?expF_eq0 ?z0 // h. move: fz; case z => // a m b =>/= /eqP => -> //. move: (nf_rev_unique v nu) => [<- <-]. by rewrite T1log_prod ?/exp_O ?expO_eq0 ?expF_eq0 ?z0 ?z1 // aux T1addn0 fz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)