proposition: Lemma exp_FO2 z m u: T1nf z -> m != 0 -> exp_O (exp_F z m) u = exp_O z u.
proof: Proof. move => nz; case: m => // n _. rewrite /exp_O expF_eq0 andbT expF_eq1 /exp_F -/exp_F //. case pu: (u==zero); first by rewrite (eqP pu) !T1muln0 !if_same. case pa: (z== zero); first by rewrite (eqP pa) T1mul0n. case pb: (z== one); first by rewrite (eqP pb) expF_1n /=. have h: forall t, T1finite t = (T1log t == zero) by case. rewrite h h (T1log_exp0 (n.+1) nz) T1mul_eq0 ! orbF //. case pc: (T1log z == zero) => //. by rewrite - 3!mulA (mulA (\F _)); rewrite mul_fin_omega. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)