theorem
proved
balanced_negate_ofOrbit_abs_iff_negativeFlag_or_balanced_zero
show as:
balanced_negate_ofOrbit_abs_iff_negativeFlag_or_balanced_zero