Removing `div_add_same`

Stream: mathlib4

[Michael Rothgang]

docs#div_add_same is the symmetrised version of a special case of docs#add_div. This used to be necessary with the old field_simp, as this was a field_simp lemma, but is no longer necessary. I this propose deprecating the old lemma: #29045 does so (and makes a lot of lines slightly shorter). Any objections?

[Michael Rothgang]

CC @Yaël Dillies since you care about naming

[Robin Arnez]

From a naming convention perspective, it sounds like add_div_left and add_div_right would be more appropriate for these two lemmas. Not sure about how useful they are though

[Bryan Gin-ge Chen]

I'm also curious whether we have any particular conventions in general about reversed variants of equalities, iffs, etc. It feels like the sort of thing that may have been discussed previously, but I haven't found anything yet.

[Violeta Hernández]

I think the general convention is "don't have them"

[Yaël Dillies]

div_add_same has always been an odd one out. same isn't convention. Instead it's self