proposition: Lemma exp_eq1 x y: T1nf x -> T1nf y -> (x^y == one) = ((x== one) || (y == zero)).
proof: Proof. move => nx ny; rewrite /T1exp;move: (nf_rev ny) => [sa sb]. rewrite [in RHS] sb T1mul_eq1 ? nf_expO // expF_eq1 // expO_eq1 T1add_eq0. by rewrite T1mul_eq0 orFb; case pa: (x== one) => //=; case ((T1split y).2). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)