proposition: Lemma expO_eq0 a b: (exp_O a b == zero) = ((a== zero) && (b != zero)).
proof: Proof. rewrite /exp_O; case pa: (a==zero). by rewrite (eqP pa); case pb: (b==zero). by case: (a== one) => //; case :(T1finite a). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)