proposition: Lemma SCH_case1 x: infinite_c x -> \2c ^c (\cf x) <> x.
proof: Proof. move => icx eq1. move: (cofinality_infinite_cardinal icx) => ic. by move: (power_cofinality2 ic); rewrite eq1; move => [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)