proposition: Lemma wf_impl_min_elt r (WF: well_founded r) B (NONEMPTY: ~ B ≡₁ ∅) : exists b, B b /\ forall b', B b' -> ~ r b' b.
proof: Proof. apply set_nonemptyE in NONEMPTY; desc. apply NNPP; intro C. induction x using (well_founded_ind WF). destruct C; eexists; split; try edone; red; ins; eauto. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom