proposition: Lemma Sorted_mono {A:Type}(R S : relation A) (Hincl : forall x y, R x y -> S x y): forall l, Sorted R l -> Sorted S l.
proof: Proof. induction 1; auto. constructor; auto. destruct H0;auto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)