proposition: Lemma choose_spec2: forall s, choose s = None -> Empty s.
proof: Proof. unfold Empty, In. intros s H. induction s as [|l IHl o r IHr]. - intro. apply empty_spec. - destruct o. + discriminate. + simpl in H. destruct (choose l). * discriminate. * destruct (choose r). -- discriminate. -- intros [a|a|]. ++ apply IHr. reflexivity. ++ apply IHl. reflexivity. ++ discriminate. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface