proposition: Lemma epsilon_fam_pr6 C (E := cnext C) (F:= Zo E epsilonp) : infinite_c C -> order_isomorphism (Lf epsilon_fam E F) (ordinal_o E) (ole_on F).
proof: Proof. move => ic. have aux:forall x,inc x (cnext C) -> inc (oopow x) (cnext C). move => x xe; apply:cnext_pow => //. exact: (cnext_leomega ic (oleR OS_omega)). move: (first_derivation_p4 ic oopow_normal aux). have -> //: (Zo E (fun z => omega0 ^o z = z)) = F. apply: Zo_exten1 => x xE; split; [move => h; split => // | by move => []]. by move/(cnextP (proj1 ic)):xE => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)