proposition: Lemma infinite_prod_pB2: cprodb Nat csucc = \2c ^c omega0.
proof: Proof. set x := (Lg Nat csucc). have fgf: fgraph x by rewrite / x; fprops. have icy: infinite_c (domain x) by rewrite /x; aw; apply: CIS_omega. have pa: cardinal_pos_fam x. move;rewrite /x; aw; move=> a adx; rewrite /x LgV//;apply: succ_positive. have pb: fg_Mle_lec x. move;rewrite /x; aw; move => a b aN bN [_ _ ab]; rewrite !LgV//. move:(CS_nat aN) (CS_nat bN) => ca cb. apply /(cleSSP ca cb); split => //. rewrite /cprodb (infinite_increasing_power fgf icy pa pb). rewrite /x infinite_prod_pB1; aw. rewrite infinite_power1_b //;exact CIS_omega. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)