proposition: Lemma min_elt_spec3: forall s, min_elt s = None -> Empty s.
proof: Proof. unfold Empty, In. intros s H. induction s as [|l IHl o r IHr]. - intro. apply empty_spec. - intros [a|a|]. + apply IHr. revert H. clear. simpl. destruct (min_elt r); trivial. case min_elt; intros; try discriminate. destruct o; discriminate. + apply IHl. revert H. clear. simpl. destruct (min_elt l); trivial. intro; discriminate. + revert H. clear. simpl. case min_elt; intros; try discriminate. destruct o; discriminate. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface