Powers of elements of groups with an adjoined zero element

We exile two lemmas about a ^ bit1 here to avoid importing unnecessary material into ring.

These lemmas can hopefully be removed entirely later.

theorem zpow_bit1₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (n : ℤ) : a ^ bit1 n = a ^ n * a ^ n * a

theorem zpow_bit1' {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (n : ℤ) : a ^ bit1 n = (a * a) ^ n * a