algebra.order.group.defs mathlib4#869

Stream: mathlib4

[Ruben Van de Velde]

mathlib4#869 has some to_additive issues I haven't diagnosed yet; if someone with more experience wants to take a look, please go ahead

[Ruben Van de Velde]

Ruben Van de Velde said:

mathlib4#869 has some to_additive issues I haven't diagnosed yet; if someone with more experience wants to take a look, please go ahead

It seems like there's an issue with the translated proof if I usesimp but not simp only