The to_additive version of this lemma was incorrectly named in Lean 3, which seemingly led to some confusion in porting