proposition: Theorem Sorted_not_in {A} : ∀ (f : A → A → Prop) a b l, (∀ x, ¬f x x) → (∀ x y z, f x y → f y z → f x z) → Sorted f [b … l] → f a b → a ∉ [b … l].
proof: Proof. intros f a b l Hirr Htran Hsort Hab Hin. destruct Hin as [Hin| Hin]. subst b. eapply Hirr; eassumption. induction l as [| c]; [ contradiction | intros ]. destruct Hin as [Hin| Hin]. subst c. apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt, _). eapply Htran in Hab; [ eapply Hirr, Hab | eassumption ]. apply IHl; [ idtac | assumption ]. eapply Sorted_minus_2nd; eassumption. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base