@[simp]

theorem Fin.compare_val {n : Nat} (a b : Fin n) : compare ↑a ↑b = compare a b

@[instance_reducible]

instance Fin.instLinearOrderPackage {n : Nat} : Std.LinearOrderPackage (Fin n)