proposition: Lemma StronglySorted_insert : forall a (R : a → a → Prop) (Q : a → a → bool) `{Transitive _ R} x xs, (forall y, Q y x = false → Q x y = true) → (forall a b, R a b <-> Q a b = true) → StronglySorted R xs → StronglySorted R (insert Q x xs).
proof: Proof. intros a R Q H x xs H1 H2 H3. generalize dependent x. induction xs as [|y ys IHys]; intros; simpl. - unfold insert. constructor; constructor. - unfold insert. destruct (Q y x) eqn:E; fold @insert. + constructor. * apply IHys; trivial. inversion H3; trivial. * apply Forall_insert; trivial. inversion H3; trivial. + constructor; trivial. constructor. * apply H2; trivial. inversion H3. apply H1 in E. assumption. * apply H1 in E. apply H2 in E. apply (@Forall_ordered a R H x y ys E). inversion H3. assumption. 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