proposition: Theorem Sorted_inv_1 {A} : ∀ (f : A → A → Prop) x l, Sorted f [x … l] → Sorted f l.
proof: Proof. intros f x l H. apply Sorted_LocallySorted_iff in H. apply Sorted_LocallySorted_iff. inversion H; [ constructor | assumption ]. Qed.
imports: Utf8 QArith NPeano Sorted Psatz