proposition: Lemma epsilon_fct_pr2 C (E:= cnext C): infinite_c C -> (forall x, inc x E -> inc (epsilon_fct x) E).
proof: Proof. move => iC. apply:next_fix_point_small => //. apply:oopow_normal. move:(cnext_pr1 (proj1 iC)); rewrite -/E; move=> [pa pb pc]. move => x xe; apply:cnext_pow => //. exact :(cnext_leomega iC (oleR OS_omega)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)