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