proposition: Lemma exp_FO1 z v n m: T1nf z -> T1nf v -> v != zero -> n != 0 -> exp_O z (v * \F n) * exp_F z m = exp_F (exp_O z v * exp_F z m) n.
proof: Proof. move => nz nv vz; case: n => // n _. elim: n => //; first by rewrite {2} /exp_F - mulA !T1muln1 // nf_expF //. move => n; rewrite /exp_F -/exp_F => <-. rewrite - mulA (mulA (exp_F z m )) exp_FO ? T1mul_eq0 //? (negbTE vz) //. by rewrite mulA expO_add -(add1n) - add_int mul_distr T1muln1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)