proposition: Lemma cnf_subset_sum_prop x y (F := (cnf_subset1 (x +#f y))): cnfp x -> cnfp y -> (inc x F /\ finite_set F).
proof: Proof. move => ox oy. move: (cnfp_nat_sum ox oy) => oz. move: (proj1(cnf_exponents_of oz)). rewrite /F/cnf_subset1; set E := cnf_exponents _ => fsE. set K := range _; set c := \csup K. have fr z: cnfp z -> finite_set (range z). move => h; apply: (finite_range (proj41 h)). apply: (finite_set_nat (proj42 h)). have nsk: forall t, inc t K -> natp t. move => t/funI_P [u /(range_gP (proj41 oz)) [o idz ->] ->]. by move/cnfpP: oz => /proj43 h; move:(proj1 (proj33(h _ idz))). have csK: cardinal_set K by move => t/nsk/CS_nat. have cN: natp c. case: (emptyset_dichot K) => kne; first by rewrite /c kne setU_0; apply: NS0. have osK: ordinal_set K by move => t/nsk/OS_nat. have fsK: finite_set K by apply: finite_fun_image; apply: fr. move:(finite_subset_ord fsK kne osK) => [n nK nv]. have nN: natp n by apply: nsk. suff: n = c by move <-. apply: (cleA (card_sup_ub csK nK)). apply: (card_ub_sup (CS_nat nN)) => t tk. by apply: (ocle3 (csK _ tk) (csK _ nK) (nv _ tk)). split; last by apply: (cnf_subset_finite fsE cN). have aux: cnf_rangep (range x). split; [ exact: (fr _ ox) | exact: (cnf_range_fgraph ox) | ]. move => t /(range_gP (proj41 ox)) [i idx ->]. by move/cnfpP: ox => /proj43; apply. move: (cnf_sort_correct aux) =>[qa qb]. move: (cnf_same_range qa ox qb) => xsr. apply/funI_P; exists (range x) => //;apply/Zo_P; split => //; apply/setP_P. move => t tr; move: (tr) => /(range_gP (proj41 ox)) [i idx tv]. have exE: inc (oexp x i) E. rewrite/E (cnf_nat_sum_p1 ox oy); apply: setU2_1. by apply/funI_P; ex_tac; rewrite tv. have le1: ocoef x i <=c Vr (x +#f y) (oexp x i). rewrite (cnf_nat_sum_p2 ox oy (oexp x i)) - (Vr_correct ox idx). apply: (csum_M0le _ (CS_nat (NS_Vr (oexp x i) ox))). rewrite tv - (proj43 ox _ idx); apply: (setXp_i exE). apply/(NleP cN) /(cleT le1); apply: (card_sup_ub csK). move/funI_P: exE =>[z zr ->];rewrite (Vr_in_range oz zr). by apply/funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)