proposition: Lemma Forall_ordered : forall a (R : a -> a -> Prop) `{Transitive _ R} x y xs, R x y -> List.Forall (R y) xs -> List.Forall (R x) xs.
proof: Proof. intros a R H x y xs H1 H2. assert (forall a, R y a -> R x a). intros z H3. transitivity y; trivial. apply List.Forall_impl with (P:=R y). intros. apply H0. assumption. 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