proposition: Lemma sortBy_sorted : forall a (R : a -> a -> Prop) (Q : a -> a -> bool) `{Transitive _ R} xs, (forall x y, Q y x = false -> Q x y = true) -> (forall a b, R a b <-> Q a b = true) -> StronglySorted R (sortBy Q xs).
proof: Proof. intros a R Q H xs H1 H2. induction xs as [|x xs IHxs]; simpl. constructor. apply StronglySorted_insert; trivial. exact (H1 x). Qed.
imports: Hask.Ltac Hask.Control.Monad Hask.Data.Eq Hask.Data.Maybe Coq.Program.Wf Coq.Sorting.Sorted Coq.Classes.RelationClasses Coq.Lists.List FunctionalExtensionality Coq.Relations.Relations Coq.Reals.ROrderedType Coq.Lists.List Coq.Sorting.Sorted Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.RelationClasses FunctionalExtensionality