proposition: Lemma choose_empty: forall s, is_empty s = true -> choose s = None.
proof: Proof. intros s Hs. case_eq (choose s); trivial. intros p Hp. apply choose_spec1 in Hp. apply is_empty_spec in Hs. elim (Hs _ Hp). Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface