proposition: Theorem OlistSkip : forall (a b : A) (L : list A), Olist (a :: b :: L) -> Olist (a :: L).
proof: Proof. intros a b L; case L. intros H'. apply OlistOne; auto. intros a0 l; case l. intros H'. apply OlistCons; auto. apply ltATrans with (y := b); auto. inversion H'; auto. inversion H'; auto. inversion H1; auto. intros a1 l0 H'; inversion H'; inversion H1. apply OlistCons; auto. apply ltATrans with (y := b); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)