proposition: Lemma choose_mem_3: is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.
proof: Proof. intros. generalize (@choose_1 s) (@choose_2 s). destruct (choose s);intros. - exists e;auto with set. - generalize (H1 (eq_refl None)); clear H1. intros; rewrite (is_empty_1 H1) in H; discriminate. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx