proposition: Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R, ∀ x y, Decision (R x y)} (X : C) : X ≠ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
proof: Proof. unfold_leibniz. apply (minimal_exists R). Qed.
imports: stdpp(relations) stdpp(options)