apply @Finite.wellFounded_of_trans_of_irrefl _ _ _
  ⟨by intro a b c rba rcb; exact IsTrans.trans c b a rcb rba⟩
  ⟨by simp [flip, IsIrrefl.irrefl]⟩
α : Type u
rel : α → α → Prop
hRefl : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl : Euclidean rel
inst✝² : Finite α
inst✝¹ : IsTrans α rel
inst✝ : IsIrrefl α rel
⊢ ConverseWellFounded rel
no goals