proposition: Lemma sort_map A (R : relation A) B (S : relation B) (f : A->B) (f_mon : Proper (R ==> S) f) : forall l, sort R l -> sort S (map f l).
proof: Proof. induction l; intro h; simpl. apply nil_sort. inversion h; subst. apply cons_sort. apply IHl. hyp. eapply lelistA_map. apply f_mon. hyp. Qed.
imports: Coq(List Morphisms Lia) CoLoR(RelUtil LogicUtil)