proposition: Lemma cnf_sum_mon_range x y (d := (cnf_degree y)): cnfp x -> cnfp_nz y -> cnf_rangep (cnf_sum_mons x y d).
proof: Proof. move => ox ynz; move: (proj1 ynz) => oy. move /cnfpP:(ox)=> aox; move/cnfpP:(oy) => aoy. move:(cnf_range_fgraph ox) => fgrx. move:(cnf_range_fgraph oy) => fgry. move: (OS_cnf_degree ynz) => od. have aux t:inc t (cnf_sum_mons x y d) -> omonomp t. case /cnf_sum_monP. + move: aoy => [ha hb hc _]. by case =>/(range_gP ha) [i /hc ok -> xs]. + move: aox => [ha hb hc _]. by case =>/(range_gP ha) [i /hc ok -> xs]. + rewrite /omonomp; move ->; aw; split; [ fprops | exact | ]. move: (NS_Vr d ox) => ra. rewrite -(cnf_coef_of_lc ynz); apply:posnat_add (posnat_lc ynz). apply:(NS_Vr _ ox). split; last exact. have H z P: cnfp z -> finite_set (Zo (range z) P). move => [ha hb _ _ ]. apply: (sub_finite_set (@Zo_S (range z) P)); apply:(finite_range ha). by apply/NatP; rewrite card_nat. by apply:setU1_finite; apply:setU2_finite; apply:H. split; first by move => t /aux; case. move => i j /cnf_sum_monP ip /cnf_sum_monP; case; case: ip. + by move => [ia _][ja _]; apply:(proj2 fgry). + by move => [_ lt1][_ lt2] sp; case: (proj2(olt_leT lt2 (proj1 lt1))). + by move => -> [_ /proj2 lt2]; aw => eq1; case:lt2. + by move => [_ lt1][_ lt2] sp; case: (proj2 (olt_leT lt1 (proj1 lt2))). + by move => [ia _][ja _]; apply:(proj2 fgrx). + by move => -> [_ /proj2 lt2]; aw => eq1; case:lt2. + by move => [_ /proj2 lt1] ->; aw; move => eq2; case:lt1. + by move => [_ /proj2 lt1] ->; aw; move => eq2; case:lt1. + by move <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)