proposition: Theorem ordered_skip : forall (a b : A) (l : list A), ordered (a :: b :: l) -> ordered (a :: l).
proof: Proof. Proof using order_trans. intros a b l; case l; clear l; auto. intros c l H; apply ordered_cons. apply order_trans with (b := b); auto. apply ordered_inv_order with (1 := H). apply ordered_inv_order with (1 := ordered_inv _ _ H). apply ordered_inv with (1 := ordered_inv _ _ H). Qed.
imports: Coq(Sorting.Permutation)