proposition: Lemma exp0nz x: x != zero -> zero ^ x = zero.
proof: Proof. by move => h; move:(exp_eq0 zero x); rewrite h /= => /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)