proposition: Lemma SCH_prop2 x (p:= cpow_less_ecb x): singular_cardinal x -> SingCardHypothesis -> ( (p -> \2c ^c x = \2c ^<c x) /\ (~ p -> \2c ^c x = cnext (\2c ^<c x))).
proof: Proof. move => sc sch; split; first by apply: cpow_less_pr10. move => pf. have aux: forall a, a <c x -> exists b, [/\ a <=c b, b <c x & \2c ^c a <c \2c ^c b]. move => a ax; ex_middle ba1. case: pf; exists a => //; move => b b1 b2. have le1:= (cpow_Meqle card2_nz b1). by ex_middle ne1; case: ba1; exists b. have le22: \2c <=c \2c by fprops. move: sc => [ix sx]. have pf':~ (exists a : Set, cpow_less_ec_prop \2c x a). by move => [a [px py]]; case: pf; exists a. move: (cpow_less_ec_pr6 ix le22 pf') => eq1. have pa: (\2c ^c (\cf (\2c ^<c x))) <c \2c ^<c x. have pb:= (cofinality_small ix). move: (aux _ (conj pb sx)) => [b [p1 p2 p3]]. by rewrite eq1; apply: (clt_leT p3); apply: cpow_less_pr2. rewrite (cpow_less_pr6a ix) - eq1. exact (sch _ (cpow_less_ec_pr0 ix le22) pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)