proposition: Lemma Exercise6_33p: cardinal (unionf alpha Mi) <c c.
proof: Proof. apply/Exercise6_33aP. have [h1 h2 h3]:=Exercise6_33o. move: Exercise6_33a6=>[sa svb sc sd]. have h5 := (cleT (proj2 (sd _ h1)) (proj1 (Exercise6_33a3))). move: (cprod_inf1 h5 Exercise6_33a); rewrite cprod2cr. apply: cleT; apply:csum_pr1_bnd => m mi. by apply/Exercise6_33aP;apply: h3. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)