proposition: Lemma natural_finite_cover x e (E:= oopow e): ordinalp e -> inc x E -> let n := cardinal (Zo (coarse E) (fun z => (P z) +#o (Q z) = x)) in natp n /\ n <> \0c.
proof: Proof. move=> oe xE; set F := Zo _ _ => n. have oE :=(OS_pow OS_omega oe). have ox:= (Os_ordinal oE xE). move: (the_cnf_p0 ox) =>[ou uv]. move: (proj2 (cnf_subset_sum_prop ou cnfp0)); rewrite (cnf_nat_sum0 ou). set G1:= (cnf_subset1 _) => h0. set G := fun_image G1 cnf_val. have h1: finite_set G by apply /finite_fun_image. move: (finite_prod2 h1 h1) => h2. have h3: sub F (G \times G). move => t /Zo_P [/setX_P [pt Pt Qt]]. move: (Os_ordinal oE Pt) (Os_ordinal oE Qt) => op oq. move: (the_cnf_p0 op)(the_cnf_p0 oq) =>[oa av][ob bv]. rewrite /natural_sum - uv; move/(cnf_val_inj (cnfp_nat_sum oa ob) ou) => s. move: (proj1(cnf_subset_sum_prop oa ob)); rewrite s => sa. move: (proj1(cnf_subset_sum_prop ob oa)); rewrite cnf_nat_sumC s => sb. by rewrite - pt -av - bv; apply: setXp_i; apply: funI_i. split; first by move: (sub_finite_set h3 h2) => /card_finite_setP. apply: card_nonempty1. have zE: inc \0o E by apply /(oltP oE); apply:(oopow_pos oe). exists (J x \0o); apply: Zo_i;first by apply :setXp_i. by rewrite pr1_pair pr2_pair natural_sum0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)