proposition: Lemma epsilon_fam_pr2'': epsilon_fam \0o = epsilon_fct (osucc omega0).
proof: Proof. rewrite epsilon_fam_pr2' /epsilon_fct. move: oopow_normal => nf. move: (normal_ofs_fix nf OS0). set u := the_least_fixedpoint_ge _ _; move => [[_ sa _] sb sc]. move: (normal_ofs_fix nf (OS_succ OS_omega)). set v := the_least_fixedpoint_ge _ _; move => [[_ sa' _] sb' sc']. apply: (oleA (sc _ (ole0x sa') sb')). apply: sc' => //; apply /oleSltP; exact : (ord_eps_p3 (conj sa sb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)