proposition: Lemma exp_FO3 z x u (w := T1div_by_omega (T1split x).1): T1nf z -> T1nf w -> (w == zero) = false -> (z == zero) = false -> exp_O (z ^ x) u = phi0( T1log (z ^x) * T1omega * u).
proof: Proof. move => nz nw xnz zz. case zo: (z== one); first by rewrite (eqP zo) exp1x T1mul0n. case uz: (u==zero); first by rewrite (eqP uz) T1muln0 expO_n0. rewrite /T1exp /exp_O -/w; set m:= (T1split x).2. set a := (if T1finite z then phi0 w else _). have na: T1nf a by rewrite fun_if !nf_phi0 !nf_mul // ? nf_log // nw if_same. have ifa: ~~ T1finite a. rewrite /a; case fz:(T1finite z) => //; first by rewrite /= xnz. move: fz; case z => // a' n' b' /=; case a' => // a'' n'' b'' _. by rewrite andbF T1mul_eq0 xnz. have ifp: T1finite (a * exp_F z m) = false. have : exp_F z m != zero by rewrite expF_eq0 zz. move: ifa; case a => // a' n' b' /=; case (exp_F z m)=> // a'' n'' b'' /=. by move=> /negbTE h _;case sa:(a'' == zero); rewrite h andFb /= ?T1add_eq0 h. case az: (a== zero); first by move: ifa; rewrite (eqP az). case ao: (a== one); first by move: ifa; rewrite (eqP ao). by rewrite zz zo uz T1mul_eq0 expF_eq0 zz andFb T1mul_eq1//az ao orbF andFb ifp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)