order of input variables

Stream: general

[Kevin Buzzard]

lemma eq_inv_mul_of_mul_eq {α : Type*} [group α] {a b c : α} : b * a = c → a = b⁻¹ * c

This is in core. More natural notation for mathematicians might be

{a x y : G} : a * x = y → x = a⁻¹ * y

but this is not quite alpha equivalent because the equivalent term has variables ordered x a y which sort of looks bonkers. Does this sort of thing matter? Does it break all the AI's if I switch them?