proposition: Lemma infinite_product_alt x : infinite_c x -> x *c x = x.
proof: Proof. move => icx; move: (proj1 (proj1 icx)) => ox. move: x ox icx; apply:least_ordinal2 => [x ox Hx] icx. have kl0: forall z, infinite_c z -> z <o x -> z *c z = z. by move => z icz zk; apply: Hx. move: (proj1 (infinite_product_aux icx kl0)) =>[bf sf tf]. by move:(card_bijection bf); rewrite sf tf - cprod2_pr1 (card_card(proj1 icx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)