well_founded typeclass

Stream: general

[Yaël Dillies]

Consider

/-- The order on `ι →₀ ℕ` is well-founded. -/
lemma lt_wf : well_founded (@has_lt.lt (ι →₀ ℕ) _) :=
subrelation.wf (sum_id_lt_of_lt) $ inv_image.wf _ nat.lt_wf

in file#data/finsupp/order. This could be generalized to ι →₀ α where α is well-founded itself. Do we want to handled well-foundedness with typeclasses?