proposition: Lemma infinite_prod_pF: cprodb omega1 \aleph = (\aleph omega1) ^c aleph1.
proof: Proof. have ic: (infinite_c omega1) by apply CIS_aleph; fprops. have oo:=(proj1 (proj1 ic)). set (X := Lg omega1 id). have sX: domain X = omega1 by rewrite /X; aw. have ha: ofg_Mlt_lto X. have fhx: fgraph (Lg omega1 id) by fprops. rewrite /X;split => //;hnf;aw; [ move=> t to | move => u v uo vo uv]; rewrite !LgV//; exact:(Os_ordinal oo to). have sr: \osup (range X) = omega1. rewrite /X identity_r. by move :(limit_nonsucc (infinite_card_limit2 ic)). have lo:limit_ordinal (domain X) by rewrite sX; exact:(aleph_limit OS1). move: (infinite_prod3_bis ic ha sX). move: (increasing_sup_limit4 ha lo) => [_ _ ->]; rewrite sr => <-. by rewrite /X; aw; apply: cprodb_exten => x xa; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)