proposition: Lemma exp_eq0 x y: x^y == zero = ((x==zero) && (y != zero)).
proof: Proof. rewrite /T1exp T1mul_eq0 expO_eq0 expF_eq0. rewrite - andb_orr; case pa: (x==zero) => //; rewrite !andTb. by case y => // a n b /=; case pb: (a== zero) => //;case: (T1split b) => u v. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)