proposition: Lemma ord_negl_opow a b: a <o omega0 ^o b -> ordinalp b -> a <<o omega0 ^o b.
proof: Proof. move => lta ob; exact:(indecomp_prop1 (indecomp_prop4 ob) lta). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)