proposition: Lemma Exercise3_5e r g: worder_on r (domain g) -> ordinal_fam g -> cardinal (osum r g) = csumb (domain g) (fun z => cardinal (Vg g z)).
proof: Proof. move=> [wo sr] ofg;move: (ofg) => alo. rewrite /osum; set h := Lgcomp _ _. have hp1: forall i, inc i (domain g) -> worder (Vg h i). rewrite /h=> i idg; rewrite LgV//; apply: ordinal_o_wor; apply: (alo _ idg). have wos: worder (order_sum r h). rewrite /h;apply: orsum_wor => //; aww. by split. by hnf; aw. move: (ordinal_o_is wos) => xx. have or: order r by fprops. have oa:(orsum_ax r h). rewrite /h;split => //;aw; hnf; aw; trivial. move=> i idg; move: (hp1 _ idg). by rewrite /h; aw; move=> [ok _]. move: (orderIS xx)=> xx1;move: (Exercise3_5c oa xx1). move: (OS_sum (conj wo sr) ofg) => r1. rewrite ordinal_o_sr /osum /fam_card_sub; move => ->. rewrite /h; aw; apply: f_equal; apply: Lg_exten; move=> i idg /=. by rewrite LgV// ordinal_o_sr //; apply: (alo _ idg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)