proposition: Lemma expF_eq1 a n: T1nf a -> (exp_F a n == one) = ((a== one) || (n == 0)).
proof: Proof. move => na; elim: n => //; first by rewrite orbT. by move => n h; rewrite /exp_F -/exp_F T1mul_eq1 // h ?orbF; case: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)