proposition: Theorem InEqSup : forall (a b : A) (L : list A), InEq a L -> Olist (b :: L) -> ltA b a.
proof: Proof. intros a b L; elim L; auto. intros H'; inversion H'; auto. intros a0 l H' H'0 H'1; inversion H'0; auto. apply ltAeqAComp with (a := b) (b := a0); auto. apply OlistSup with (L := a0 :: l); auto with datatypes core. apply H'; auto. apply OlistSkip with (b := a0); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)