proposition: Lemma Exercise3_5f r g: worder_on r (domain g) -> ordinal_fam g -> finite_set (substrate r) -> cardinal (oprod r g) = cprodb (domain g) (fun z => cardinal (Vg g z)).
proof: Proof. move=> wosr ofg fsr; move: (ofg) => alo; move: (wosr) => [wo sr]. rewrite /oprod; 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_prod r h). by rewrite /h;apply: orprod_wor => //=;aw; fprops; hnf; aw. move: (ordinal_o_is wos) => xx. have oa:(orprod_ax r h). rewrite /h;split => //; hnf; aw; trivial; move=> i idg. by move: (hp1 _ idg); rewrite /h; aw; move=> [ok _]. move: (orderIS xx)=> xx1;move: (Exercise3_5d oa xx1). move: (OS_prod wosr ofg fsr) => r1. rewrite (ordinal_o_sr (oprod r g));rewrite /oprod /fam_card_sub => ->. rewrite /h; aw; apply: f_equal; apply: Lg_exten; move=> i idg /=; rewrite LgV//. by rewrite ordinal_o_sr //; apply: (alo _ idg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)