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