proposition: Lemma min_elt_2 : forall (s : t) (x y : elt), min_elt s = Some x -> In y s -> ~ E.lt y x.
proof: Proof. intros s x y; unfold min_elt; case (M.min_elt s). - unfold For_all; simple destruct s0; intros; injection H; intros; subst; firstorder. - intros; discriminate H. Qed.
imports: FSetInterface