Also fix one use of inj _ from before !408 (merged). There's one leftover from sum_ofe_mixin, but I'd leave it alone tho it's pretty weird:
$ git grep '\binj\b _'
theories/algebra/ofe.v: + destruct (Hx 0); constructor; apply equiv_dist=> n; by apply (inj _).because this would be the fix:
- + destruct (Hx 0); constructor; apply equiv_dist=> n; by apply (inj _).
+ + destruct (Hx 0); constructor; apply equiv_dist=> n; by [apply (inj inl)|apply (inj inr)].