Equality from injective

The following lemma can be useful and I did not find an equivalent in mathcomp
```rocq-prover
Lemma injectiveE A B (f : A -> B) : injective f ->
  forall x y, (f x = f y) = (x = y).
```
Although I do not know if it could be useful anywhere inside the library, both uses of inj_eq are used on goals where boolean equality was already present.