proposition: Lemma min_elt_1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s.
proof: Proof. intros s x; unfold min_elt; case (M.min_elt s). - simple destruct s0; intros; injection H; intros; subst; intuition. - intros; discriminate H. Qed.
imports: FSetInterface