theorem pow_two_mul_abs {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (n : ℕ) (a : α) : |a| ^ (2 * n) = a ^ (2 * n)