proposition: Lemma infinite_product_aux k (lo:= graph_on ord_pair_le (coarse k)) (f := ordinal_iso lo): infinite_c k -> (forall z, infinite_c z -> z <o k -> z *c z = z) -> bijection_prop f (coarse k) k /\ (forall x y, inc x (source f) -> inc y (source f) -> (glt lo x y <-> (Vf f x) <o (Vf f y))).
proof: Proof. move => ik hrec. move: (ik) => [[ok _] _]; move: (ik) => [ck _]. have pa: (forall a, inc a (coarse k) -> ord_pair_le a a). move => a /setX_P [pa p1a p2a]; apply: ordering_pair4; hnf;split => //. apply: (Os_ordinal ok p1a). apply: (Os_ordinal ok p2a). move: (wordering_pr well_ordering_pair pa); rewrite -/lo; move=> [los low]. move: (OS_ordinal los) => ot. move:(ordinal_isomorphism_exists los); rewrite -/f => oisf. move: (oisf) => [or1 or2 [bf sf tf] isf]. rewrite (ordinal_o_sr (ordinal lo)) in tf. move: (bf) => [injf [ff sjf]]. have fp1: forall a, inc a (source f) -> ordinalp (Vf f a). move => a asf; move: (Vf_target ff asf); rewrite tf. apply: (Os_ordinal ot). have oifp: forall x y, inc x (source f) -> inc y (source f) -> (glt lo x y <-> (Vf f x) <o (Vf f y)). move => a b asf bsf; apply:(iff_trans (order_isomorphism_siso oisf asf bsf)). split. move => [] /ordo_leP [_ _ qa] pb; split => //;split;fprops. move => [[_ _ qd] qa]; split => //. by apply/ordo_leP;split => //; rewrite tf; apply: (Vf_target ff). have otf: ordinalp (target f) by ue. have pb: forall t, inc t (source f) -> (Vf f t) =c (Zo (source f) (fun z => (glt lo z t))). move => t tsf; symmetry;apply /card_eqP. set A := (Zo (source f) ((glt lo)^~ t)). have As: sub A (source f) by apply Zo_S. move: (Vf_target ff tsf) => wt. have ra: restriction2_axioms f A (Vf f t). split => //; [by apply (ordinal_transitive otf wt) | move => w ]. move => /(Vf_image_P ff As) [u /Zo_P [usf lt] ->]. by move: lt; rewrite (oifp _ _ usf tsf); move /oltP0 =>[_ _]. move: (restriction2_fi injf ra). set g := restriction2 f A (Vf f t) => injg. have sg: source g = A by rewrite /g/restriction2; aw. have tg: target g = Vf f t by rewrite /g/restriction2; aw. exists g; split => //; split => //; split; first by fct_tac. rewrite sg tg; move=> y ytg. move: (ordinal_transitive otf wt ytg) => ytf. move: (sjf _ ytf) => [w wsf wv]; move: (fp1 _ tsf) => ow. have wa: inc w A. by apply: Zo_i => //; rewrite (oifp _ _ wsf tsf) - wv; apply /oltP. exists w => //; rewrite restriction2_V //. have pc: forall t, inc t (source f) -> cardinal (Vf f t) <c k. move => t tsf; rewrite (pb _ tsf). set S := (Zo (source f) ((glt lo)^~ t)). have qa: sub S (coarse (osucc (ord_pair_max t))). move => v /Zo_P [vs [/graph_on_P1 [_ _ le] _]];exact (ordering_pair3 le). move: (sub_smaller qa). move: tsf; rewrite sf low => tsf1. set a := (osucc ((ord_pair_max t))). rewrite /coarse - cprod2_pr1 - cprod2cl - cprod2cr. move=> le1; apply: (cle_ltT le1). case: (finite_or_infinite (CS_cardinal a)) => fca. apply: clt_fin_inf => //. apply /NatP; apply: NS_prod; fprops. have ak : a <o k. apply /oltP => //. move: (infinite_card_limit2 ik) => [_ _]; apply. move: (tsf1) => /setX_P [_ i1 i2]. by case: (ordering_pair1 (proj31 (pa _ tsf1))); move => [cd ->]. move: ak (ak) => [[oa _ _] _]. move/ (ocle2P ck oa) => cak. move: (oclt cak) => lt1. by rewrite (hrec _ fca lt1). rewrite -low - sf;split => //; saw. have pd: sub (ordinal lo) k. move => t; rewrite - tf => ttf; move: (sjf _ ttf) => [v vsf ->]. apply/(oltP ok) /(ocle2P ck (fp1 _ vsf)). exact: (pc _ vsf). move: (card_bijection bf); rewrite sf low - cprod2_pr1 => pe. rewrite tf; ex_middle xx. have /(ocle2P ck otf) : target f <o k by split => //; rewrite tf => //. by move: (cleNgt (cprod_M1le ck (infinite_nz ik))); rewrite pe. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)