IsWellOrder of RelIso

Stream: Is there code for X?

[Nir Paz]

Is the a quick consequence of something we have? I'm having surprisingly much trouble with it

example {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop}
    (h : IsWellOrder α r) (f : r ≃r s) : IsWellOrder β s := sorry

[Yaël Dillies]

docs#RelIso.IsWellOrder.preimage but there's a better one

[Nir Paz]

Ah, docs#RelEmbedding.isWellOrder is perfect