proposition: Lemma exp_FO z n v: v != zero -> exp_F z n * exp_O z v = exp_O z v.
proof: Proof. move /negbTE => vz. elim: n => //; first by rewrite T1mul1n. move => n; rewrite /exp_F -/exp_F - mulA; move => ->. rewrite /exp_O vz; case: eqP;[ by move => -> | case: eqP; first by move ->]. case fz: (T1finite z). move: fz; case z => // a' n'' b' /=;rewrite vz andbF => /eqP -> //. move: fz;rewrite - mulA; case z => // a' n'' b'; rewrite /T1log. rewrite /T1finite /phi0 {1} /T1mul T1mul_eq0 T1mul_eq0 vz => -> /=. by rewrite add_simpl3 // vz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)