proposition: Theorem OlistSup : forall (a : A) (L : list A), Olist (a :: L) -> forall b : A, In b L -> ltA a b.
proof: Proof. intros a L; elim L; simpl in |- *; auto. intros H' b H'0; elim H'0. intros a0 l H' H'0 b H'1; Elimc H'1; intros H'1; [ rewrite <- H'1 | idtac ]; auto. inversion H'0; auto. apply H'; auto. apply OlistSkip with (b := a0); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)