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: Coq.Sorting.Sorted Coq.Sorting.Permutation Category.Lib Category.Theory.Functor Category.Theory.Coq.Functor Category.Theory.Coq.Functor.Proofs Category.Theory.Coq.List Category.Theory.Coq.Maybe