finset on linear order to list?

Stream: Is there code for X?

[Rémi Bottinelli]

Hey, is there some api around something like this? Thanks!

namespace finset

variables  {X : Type*} [linear_order X] (s s' t : finset X) (h : s ≤ t)

def to_sorted_list : list X := sorry

lemma to_sorted_list_sorted : s.to_sorted_list.pairwise (≤) := sorry
lemma to_sorted_list_mono : s.to_sorted_list <+ t.to_sorted_list := sorry
lemma to_sorted_list_strictly_sorted : s.to_sorted_list.pairwise (<) := sorry
lemma to_sorted_list_union : (s \cup s').to_sorted_list = (s.to_sorted_list ++ s'.to_sorted_list).sort := sorry
lemma to_sorted_list_sep_union (h' : \forall x \in s, \forall y \in s', x < y) : (s \cup t).to_sorted_list = s.to_sorted_list ++ s'.to_sorted_list := sorry

end finset