proposition: Lemma cnf_sum_prop9 x y (d := cnf_degree y) (k := position_in_cnf x d): cnfp x -> cnfp_nz y -> ~(inc d (domain (range x))) -> x +f y = cnf_nm y (cnf_ns x k).
proof: Proof. move => ox ynz dd. have oy := proj1 ynz. move: (OS_cnf_degree ynz); rewrite -/d => od. move: (position_in_cnf_prop ox od); rewrite -/k. move => [kdx kp1 kp2]. move: (cnfp_cnf_ns ox kdx) => oz. rewrite (cnf_sum_prop8 ox ynz) -/k; symmetry; apply: (cnf_nm_sum oy oz). move => i j /(NltP (proj42 oy)) idy jdz. apply:(ole_ltT (cnf_degree_greatest oy idy)); rewrite -/d. move: jdz;rewrite /cnf_ns/cnf_s Lgd /oexp => jl1. have nN := proj42 ox. case: (cle_eqVlt kdx) => ckn. by move: jl1; rewrite - ckn cdiff_nn => /clt0. move/(NltP (NS_diff k nN)): (jl1) => jdz; rewrite LgV//. case: kp2; first by move=> kv; case: (proj2 ckn). move/ole_eqVlt; case => cd. case:dd; apply/funI_P; rewrite cd; exists (Vg x k) => //. by apply:(inc_V_range (proj41 ox)); apply/NltP. have le1: k <=c j +c k by apply:(csum_Mle0 _ (proj31_1 ckn)). have le2: j +c k <c domain x. by move:(csum_Meqlt (NS_lt_nat ckn nN) jl1); rewrite (cdiff_pr kdx) csumC. apply(olt_leT cd). exact: (CNF_exponents_M (proj42 ox) (proj1 (proj44 ox)) le1 le2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)