proposition: Theorem Sorted_minus_2nd {A} : ∀ (f : A → A → Prop) x₁ x₂ xl, (∀ x y z, f x y → f y z → f x z) → Sorted f [x₁; x₂ … xl] → Sorted f [x₁ … xl].
proof: Proof. intros f x₁ x₂ l Ht H. apply Sorted_LocallySorted_iff. destruct l as [| x₃]; [ constructor | intros ]. constructor. apply Sorted_LocallySorted_iff. do 2 apply Sorted_inv_1 in H. assumption. apply Sorted_inv_2 in H; destruct H as (Hlt₁, H). apply Sorted_inv_2 in H; destruct H as (Hlt₂, H). eapply Ht; eassumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz