proposition: Lemma sorted_In : forall i X, Sorted lt (i::X) -> forall j, In j X -> i < j.
proof: Proof. intros. apply Sorted_StronglySorted in H. apply StronglySorted_inv in H. destruct H. rewrite Forall_forall in H1. auto. red. intros; abstract lia. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)