proposition: Lemma max_elt_2: forall s x y, max_elt s = Some x -> In y s -> ~ E.lt x y.
proof: Proof. unfold In. induction s as [|l IHl o r IHr]; intros x y H H'. - discriminate. - simpl in H. case_eq (max_elt r). + intros p Hp. rewrite Hp in H. injection H as [= <-]. destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial. + intro Hp; rewrite Hp in H. apply max_elt_3 in Hp. destruct o. * injection H as [= <-]. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). * destruct (max_elt l). -- injection H as [= <-]. destruct y as [z|z|]. ++ elim (Hp _ H'). ++ apply (IHl e z); trivial. ++ discriminate. -- discriminate. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface