is_atomic_of_well_founded

Stream: Is there code for X?

[Scott Morrison]

Can anyone help me with the following?

import order.atoms

example {α : Type*} [partial_order α] [order_bot α] (h : well_founded ((>) : α → α → Prop)) :
  is_atomic α := sorry

[Junyan Xu]

import order.atoms

example {α : Type*} [partial_order α] [order_bot α] (h : well_founded ((<) : α → α → Prop)) :
  is_atomic α :=
⟨ λ a, or_iff_not_imp_left.2 $
  λ ha, let ⟨b,hb,hm⟩ := h.has_min { b | b ≠ ⊥ ∧ b ≤ a } ⟨a,ha,le_rfl⟩ in
  ⟨b, ⟨hb.1, λ c, not_imp_not.1 $ λ hc hl, hm c ⟨hc,hl.le.trans hb.2⟩ hl⟩, hb.2⟩ ⟩

[Scott Morrison]

#13967