proposition: Lemma infinite_prod_pB1: union (range (Lg Nat csucc)) = omega0.
proof: Proof. rewrite Lg_range; set_extens t. move => /setU_P [z tz /funI_P [u u1 uv]]. rewrite uv in tz; exact:(NS_inc_nat (NS_succ u1) tz). move => tu; apply/setU_P; exists (osucc t); fprops. rewrite - (succ_of_nat tu); apply /funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)