[`Order`] Every chain is finite iff well-founded in both directions

[SnirBroshi]

Generalize

• IsChain.linearOrder
• Finite.of_wellFoundedLT_of_wellFoundedGT
• IsChain.finite_of_wellFoundedLT_of_wellFoundedGT

to any relation, and make IsChain.finite_of_wellFoundedLT_of_wellFoundedGT an iff:

-- generalized version of `IsChain.linearOrder`
theorem IsChain.asymm {α : Type*} {r : α → α → Prop} [Std.Irrefl r] [IsTrans α r] {s : Set α}
    (hs : IsChain r s) : Std.Asymm (r.onFun (↑) : s → s → Prop) := by
  sorry
theorem IsChain.total {α : Type*} {r : α → α → Prop} [Std.Irrefl r] [IsTrans α r] {s : Set α}
    (hs : IsChain r s) : Std.Total (r.onFun (↑) : s → s → Prop) := by
  sorry

-- generalized `Finite.of_wellFoundedLT_of_wellFoundedGT`
-- TODO: could we weaken `Total` to `Trichotomous`?
theorem Finite.of_wellFounded_of_wellFounded_flip {α : Type*} {r : α → α → Prop} [IsTrans α r]
    [Std.Asymm r] [Std.Total r] [IsWellFounded α r] [IsWellFounded α (flip r)] : Finite α := by
  -- try using `exists_increasing_or_nonincreasing_subseq`, like the original uses `Infinite.exists_strictMono_or_strictAnti`
  sorry

-- generalized iff version of `IsChain.finite_of_wellFoundedLT_of_wellFoundedGT`
theorem wellFounded_and_wellFounded_flip_iff {α : Type*} (r : α → α → Prop) :
    WellFounded r ∧ WellFounded (flip r) ↔ ∀ s : Set α, IsChain r s → s.Finite := by
  sorry

Try using wellFounded_iff_isEmpty_descending_chain or RelEmbedding.wellFounded_iff_isEmpty.