proposition: Lemma T1log_exp0 x n: T1nf x -> T1log (exp_F x n) = (T1log x) * (\F n).
proof: Proof. elim: n => // n h; rewrite /exp_F -/exp_F. case xz: (x==zero); first by rewrite (eqP xz) T1mul0n //. move => nx;rewrite T1log_prod ? expF_eq0 ? xz // h // -add1n -add_int mul_distr. by rewrite T1muln1 // nf_log. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)