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