Get dichotomy from well order

Stream: lean4

[Nir Paz]

I must be missing something, how can I prove this more easily?

import Mathlib

variable {α : Type*}

def r : α → α → Prop := sorry

instance : IsWellOrder α r := sorry

example (a b : α) (hne : a ≠ b) : r a b ∨ r b a := by
  have : IsTrichotomous α r := IsStrictTotalOrder.toIsTrichotomous
  have := this.trichotomous a b
  simp [hne] at this
  exact this

[Yaël Dillies]

have := total_of r a b?

[Yaël Dillies]

Ah no sorry you have a non-reflexive relation. Yes, it's a bit of a pain. Most people use canonical order, in which case the lemma is docs#Ne.lt_or_lt

[Nir Paz]

Would it be ok to add something like

theorem total_of_wellOrder [IsWellOrder α r] {a b : α} (h : a ≠ b) : r a b ∨ r b a

[Nir Paz]

I want to work with multiple well orders on the same type so I don't want to use canonical orders