proposition: Theorem Olistf : forall L : list A, Olist L -> Olist (map f L).
proof: Proof. intros L H'; elim H'; simpl in |- *; auto. intros a b L0 H'0 H'1 H'2. apply OlistCons; auto. apply ltAeqAComp with (a := a) (b := b); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)