proposition: Lemma ord_eps_p3 x: epsilonp x -> omega0 <o x.
proof: Proof. move: oopow1 => o1 [ox oex]; move: (proj2 (olt_1omega)); rewrite - o1. move:(oopow_pos ox); rewrite oex => xp. case: (oone_dichot xp) => xo; first by rewrite - xo oex. move => _; rewrite - oex; exact: (opow_Mo_lt xo). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)