why is image_add_const_Ici backwards?

Stream: general

[Scott Morrison]

It seems image_add_const_Ici and its relatives have a gratuitous reversal of the addition. Does anyone know why?

@[simp] lemma image_add_const_Ici : (λ x, x + a) '' Ici b = Ici (a + b) := by simp [add_comm]

[Yury G. Kudryashov]

I don't remember why I did this. Feel free to change (if not changed yet).