proposition: Lemma infinite_regularP x: infinite_c x -> (regular_cardinal x <-> forall f, csum_of_small1 x f -> cardinal (domain f) <c x -> csum f <c x).
proof: Proof. move => ix. have ox: ordinalp x by move: ix => [[ok _] _]. have x2: \2c <=c x by apply: infinite_ge2. move: (cofinality_c_rw x2) => [p3 [f [f1 f2 f3] p5]]. have cc:= proj31 p3. split => h; last first. split;[exact | case:(cle_eqVlt p3) => //; rewrite -(card_card cc) -f2 => lt]. by case: (proj2 (h f f1 lt)); rewrite f3. move: h=> [_ rx] g gp [le1 ba]. move: (csum_commutative1 gp) => [h [h1 h2 h3 h4]]. split. move: (csum_of_small_b2 h1); rewrite - h3 h2 => p6. exact: (cleT p6 (cprod_inf1 le1 ix)). move => cs; rewrite cs in h3; case: ba; apply: oleA. by move: (ocle le1). rewrite - rx; apply: p5; [ by apply: OS_cardinal; fprops | by exists h]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)