proposition: Lemma epsilon_fct_pr3 (e:= epsilon_fct \1o) : epsilonp e /\ forall x, epsilonp x -> e <=o x.
proof: Proof. move: (epsilon_fct_pr0 OS1) => [/proj32 pa pb pc]; split; first exact. move => x h; move: (ole_ltT (ole0x OS_omega) (ord_eps_p3 h)) => x1. by move: h => [ox oex]; apply: pc => //; apply/oge1P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)