proposition: Lemma mmin_spec : forall `{Inhab A} (le:binary A) (P:A->Prop) m, m = mmin le P -> ex P -> ex (lower_bound le P) -> bounded_has_minimal le -> min_element le P m.
proof: Proof. Proof using. intros. subst. unfold mmin. epsilon* m. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation LibOrder LibEpsilon)