proposition: Lemma regular_alt_prop X x: fgraph X -> allf X (fun z => z <o x) -> (domain X) <o x -> regular_cardinal x -> osum (ordinal_o (domain X)) X <o x.
proof: Proof. move => fgX Xb dxb reg. have icx := proj1 reg. have H t: t <o x -> cardinal t <c x. by move => tx; apply/(ocle2P (proj1 icx) (proj31_1 tx)). have od := proj31_1 dxb. set r := (ordinal_o (domain X)). have ha: worder_on r (domain X). split; [exact (ordinal_o_wor od) | by rewrite ordinal_o_sr ]. have ofX: ordinal_fam X by move => i /Xb [[]]. have os: ordinalp (osum r X) by apply: OS_sum. apply/(ocle2P (proj1 icx) os); rewrite (osum_cardinal_gen ha ofX). set f := (Lg (domain X) (fun z => cardinal (Vg X z))). have : cardinal (domain f) <c x by rewrite /f; aw; apply:H. have :csum_of_small1 x f. by rewrite/f;split; fprops; hnf; aw => i idx; rewrite LgV//; apply:(H _ (Xb _ idx)). by move /(infinite_regularP icx): reg; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)