proposition: Lemma exp_prod x y z: T1nf z -> T1nf x -> T1nf y -> z ^(x *y) = (z ^x) ^y.
proof: Proof. move => nz nx ny. move:(nf_rev_prod nx ny). rewrite {1 2} /T1exp. set u := T1div_by_omega (T1split y).1; set n := (T1split y).2. set v := T1div_by_omega (T1split x).1; set m := (T1split x).2. set w := T1div_by_omega (T1split (x*y)).1; set p := (T1split (x* y)).2. move:(nf_rev nx); rewrite -/v -/m; move => [nv xv]. case z1: (z== one); first by rewrite (eqP z1) exp1x !expO_1n !expF_1n. case vz: (v== zero). have ->: x = \F m by move: xv; rewrite (eqP vz) T1muln0. case mz: (m==0). by move => [-> ->]; rewrite (eqP mz) expx0 expO_n0 expO_1n expF_1n. by move => [-> ->]; rewrite expx_nat expF_mul exp_FO2 // mz. move => H. have ->: w = v * T1omega * u + v * \F n. by move:H;case h: (n== 0); move => [-> _] //;rewrite (eqP h) T1muln0 T1addn0. have ->: exp_F (z ^ x) n = (exp_O z (v * \F n) * exp_F z p). move: H; case h: (n== 0); move => [_ ->]. by rewrite (eqP h) T1muln0 expO_n0. rewrite /T1exp -/v -/m exp_FO1 ? vz ? h//. case uz: (u== zero); first by rewrite (eqP uz) !T1muln0 expO_n0 T1mul1n. have xnz: x != zero by rewrite xv T1add_eq0 T1mul_eq0 vz orFb andFb. case z0: (z==zero). rewrite (eqP z0) (exp0nz xnz) /exp_O eqxx uz T1mul0n T1add_eq0 !T1mul_eq0. by rewrite uz vz T1mul0n. rewrite mulA; congr T1mul; rewrite (exp_FO3 u nz nv vz z0). case fz: (T1finite z). by rewrite /exp_O z0 z1 fz xv T1log_exp2 //mul_phi0. have ez: forall w, exp_O z w = phi0 (T1log z * T1omega * w). by move => t ;rewrite /exp_O; move: fz;case z => // a k b; case a. rewrite ez ez - mul_phi0 T1log_exp1 ? fz// - !mulA. by rewrite -!mul_distr (mulA x) xv mul_sum_omega ? vz // -!mulA -!mul_distr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)