proposition: Lemma expF_eq0 a n: (exp_F a n == zero) = ((a== zero) && (n != 0)).
proof: Proof. elim: n => //; first by rewrite andbF. by move => m /=; rewrite T1mul_eq0 => ->; rewrite andbC andKb andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)