proposition: Theorem ordered_trans_app : forall (a b : A) (l1 l2 : list A), ordered (l1 ++ l2) -> In a l1 -> In b l2 -> order a b.
proof: Proof. Proof using order_trans. intros a b l1 l2; generalize a b; elim l1; simpl in |- *; clear l1 a b. intros a b H H1; case H1. intros c l H a b H0 [H1| H1] H2. rewrite <- H1; apply ordered_trans with (1 := H0); auto with datatypes. apply H; auto. apply ordered_inv with (1 := H0); auto. Qed.
imports: Coq(Sorting.Permutation)