proposition: Lemma infinite_prod_pB: cprodb Nat csucc = \2c ^c omega0.
proof: Proof. move:CIS_omega => io. apply: cleA. rewrite - (infinite_power1_b io). rewrite - cprod_of_same. apply: cprod_increasing; aww. move=> x xN; rewrite !LgV//; apply:cle_fin_inf => //. by apply /NatP; apply: NS_succ. rewrite - cprod_of_same infinite_prod_pA. apply: cprod_increasing; aww => x xN; rewrite !LgV//. rewrite - succ_one - succ_zero. apply:cleSS; apply: cleSS. apply:(cle0n xN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)