Def Equiv.embeddingFinSucc

feat: Equivalence between embeddings of `Fin (n + 1)`, and embeddings of `Fin n` together with a value outside the range. (#12151)