proposition: Lemma Sphi_bounded C (E :=cnext C) x y: infinite_c C -> inc x E -> inc y E -> inc (Sphi y x) E.
proof: Proof. move => ic xe ye. have [ha hb]:= (all_der_pow_aux). have oE:= (proj1 (CS_cnext (proj1 ic))). have ox:= Os_ordinal oE xe. have oy:= Os_ordinal oE ye. have h: card_max x y <=c C. rewrite /card_max /omax/Gmax; Ytac pa; last Ytac pb. + by rewrite cardinal_Nat; apply/infinite_c_P2. + by move/(cnextP (proj1 ic)): ye => []. + by move/(cnextP (proj1 ic)): xe => []. move: (omax_p2 (OS_omax ox oy)) => []; rewrite -/(card_max x y) -/C1 => sa _. move: (proj1 (CS_cnext (proj1 sa))) => oF. have sc: sub (cnext (card_max x y)) E. move => t /(cnextP (proj1 sa)) [sa' sb]; apply/(cnextP (proj1 ic)). split => //; exact: (cleT sb h). by move:(all_der_p3 ha hb ox oy) => /sc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)