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: 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