Theorems about equality in Fin.

theorem Fin.eq_of_veq {n : ℕ} {i : Fin n} {j : Fin n} : i.val = j.val → i = j

theorem Fin.veq_of_eq {n : ℕ} {i : Fin n} {j : Fin n} : i = j → i.val = j.val

theorem Fin.ne_of_vne {n : ℕ} {i : Fin n} {j : Fin n} (h : i.val ≠ j.val) : i ≠ j

theorem Fin.vne_of_ne {n : ℕ} {i : Fin n} {j : Fin n} (h : i ≠ j) : i.val ≠ j.val