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