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