for n being Nat
for c1 being Complex holds ((((c1 |^ n) / 2) + (c1 / 2)) |^ 2) - ((((c1 |^ n) / 2) - (c1 / 2)) |^ 2) = c1 |^ (n + 1)