proposition: Lemma minimal_exists R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) : X ≢ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
proof: Proof. pattern X; apply set_ind; clear X. { by intros X X' HX; setoid_rewrite HX. } { done. } intros x X ? IH Hemp. destruct (set_choose_or_empty X) as [[z ?]|HX]. { destruct IH as (x' & Hx' & Hmin); [set_solver|]. destruct (decide (R x x')). - exists x; split; [set_solver|]. eapply union_minimal; [eapply singleton_minimal|by eapply minimal_weaken]. - exists x'; split; [set_solver|]. by eapply union_minimal; [apply singleton_minimal_not_above|]. } exists x; split; [set_solver|]. rewrite HX, (right_id _ (∪)). apply singleton_minimal. Qed.
imports: stdpp(relations) stdpp(options)