proposition: Theorem Sorted_inv_2 {A} : ∀ (f : A → A → Prop) x y l, Sorted f [x; y … l] → f x y ∧ Sorted f [y … l].
proof: Proof. intros f x y l H. apply Sorted_LocallySorted_iff in H. rewrite Sorted_LocallySorted_iff. inversion H; subst a b l0. split; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz