proposition: Lemma max_elt_1: forall s x, max_elt s = Some x -> In x s.
proof: Proof. unfold In. induction s as [| l IHl o r IHr]; simpl. - intros. discriminate. - intros x. destruct (max_elt r); intros. + injection H as [= <-]. apply IHr. reflexivity. + destruct o; simpl. * injection H as [= <-]. reflexivity. * destruct (max_elt l); simpl in *. -- injection H as [= <-]. apply IHl. reflexivity. -- discriminate. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface