proposition: Lemma infinite_increasing_power x (y := domain x): fgraph x -> infinite_c y -> cardinal_pos_fam x -> fg_Mle_lec x -> cprod x = (\csup (range x)) ^c y.
proof: Proof. move => fx cy alz xi. have osr: cardinal_set (range x). move => t /(range_gP fx) [z zy ->]; exact: (proj32_1(alz _ zy)). apply: cleA. rewrite - cprod_of_same /cst_graph; apply: cprod_increasing => //; aww. move=>t td; rewrite LgV//. by apply: card_sup_ub => //; apply /(range_gP fx); ex_tac. move: (infinite_product_prop2 cy); set f := ordinal_iso _. move => [[bf sf tf] fp]. set g:= Lg y (fun z=> fun_image y (fun t => (Vf f (J t z)))). have ff: function f by fct_tac. have pa: partition_w_fam g (domain x). rewrite /g; split;fprops. apply: mutually_disjoint_prop; aw. move=> i j z iy jy; rewrite !LgV//. move=> /funI_P [a ay av] /funI_P [b iby bv]. rewrite av in bv. have asf: inc (J a i) (source f) by rewrite sf; fprops. have bsf: inc (J b j) (source f) by rewrite sf; fprops. exact (pr2_def (bij_inj bf asf bsf bv)). set_extens t. move /setUb_P; aw; move => [a ay];rewrite LgV//;move /funI_P => [b ny ->]. rewrite -/y -tf; Wtac; rewrite sf; fprops. rewrite -/y -tf => ytf; move: (bij_surj bf ytf) => [z zs zv]. move: zs; rewrite sf => /setX_P; rewrite -tf; move => [pz za zb]. apply /setUb_P; exists (Q z) => //;aw;trivial;rewrite LgV//; apply /funI_P. by exists (P z) => //; rewrite pz. rewrite (cprod_An pa). rewrite {1} /g; aw. rewrite - cprod_of_same /cst_graph; apply: cprod_increasing => //;aw; trivial. move=> a ay; rewrite LgV // LgV //. set h := (restr x (Vg g a)). have fgr: fgraph h by rewrite /h;fprops. have s1: sub (Vg g a) (domain x). rewrite /g => t; rewrite LgV//; move /funI_P => [z zy ->]; rewrite -/y - tf. Wtac; rewrite sf; fprops. have pb: (forall b, inc b (domain h) -> \0c <c Vg h b). rewrite /h restr_d // => b bv. rewrite restr_ev //; exact: (alz _ (s1 _ bv)). move: (compare_sum_prod5 fgr pb); rewrite -/h => le1. have csh: cardinal_set (range h). move => t /(range_gP fgr) [u ud ->]; exact: (proj32_1 (pb _ ud)). apply: (cleT _ le1). apply card_ub_sup => //; first by apply: CS_sup. move => i /(range_gP fx) [j jdx ->]. rewrite -/y -tf in jdx; move:(bij_surj bf jdx) => [z zf ->]. move: (zf); rewrite sf => /setX_P [pz py qy]. move: (infinite_card_limit2 cy) => [oy _ yp]. have op: ordinal_pair z by split => //; apply: (Os_ordinal (proj1 (proj1 cy))). set b0 := (ord_pair_max z); set b := osucc b0. have ib0y: inc b0 y by rewrite /b0;case: (ordering_pair1 op); move=> [_ -> ]. have iby: inc b y by apply yp. move: (Os_ordinal oy iby) (Os_ordinal oy ay) => ob oa. have opab: ordinal_pair (J b a) by split => //; aww. have bsba:= (proj1 (omax_p1 ob oa)). have ult: ord_pair_max z <o omax b a. apply: (olt_leT _ bsba); exact (oltS (Os_ordinal oy ib0y)). have nzj: z <> J b a. by move => zj; case: (proj2 ult); rewrite zj/ord_pair_max; aw. have sa: inc (Vf f (J b a)) (Vg g a) by rewrite /g LgV//; apply /funI_P; ex_tac. have wy: inc (Vf f z) y by rewrite - tf; Wtac. have wy': inc (Vf f (J b a)) y by rewrite - tf; Wtac; rewrite sf; fprops. have jsf: inc (J b a) (source f) by rewrite sf; fprops. have sb: Vf f z <o Vf f (J b a). rewrite -(fp _ _ zf jsf); split => //. have hw:ord_pair_le z (J b a) by split => //; left; rewrite /ord_pair_max; aw. rewrite/coarse;apply /graph_on_P1; split; fprops; apply /setX_P;split => //. apply: (cleT (xi _ _ wy wy' (proj1 sb))). apply: card_sup_ub => //; apply /(range_gP fgr). exists (Vf f (J b a)); rewrite /h => //; aw;trivial; rewrite LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)