Small change to inject≤

```agda
inject≤ : ∀ {m n} → Fin m → m ℕ.≤ n → Fin n
inject≤ {n = zero} zero ()
inject≤ {n = suc n} zero le = zero
inject≤ (suc i) (s≤s le) = suc (inject≤ i le)
```
https://agda.github.io/agda-stdlib/Data.Fin.Base.html#3219

This way, we avoid to need to pattern match on ```le``` , which can be hard to do on a proof, we would need to abstact over ```le``` so as to pattern match.