Finite_Totally_Ordered_Set_is_Well_Ordered

import Mathlib.Order.WellFounded
import Mathlib.Data.Fintype.Basic
import Mathlib.Order.Basic

theorem Finite_Totally_Ordered_Set_is_Well_Ordered {α : Type _} [LinearOrder α] [Fintype α] : IsWellOrder α (· < ·) := by sorry