proposition: Lemma ord_negl_p2 b e: b <o omega0 -> \0o <o e -> b <<o (oopow e).
proof: Proof. move => bo /oge1P ne0. move:(opow_Mo_le ne0); rewrite oopow1 => bb. exact:(ord_negl_sum' (proj31_1 bo) (osum_int_omega bo) bb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)