proposition: Lemma CNF_sum_pr1 x y n: cnfp x -> cnfp_nz y -> n <c domain x -> cnf_degree y <o oexp x n -> (n = \0c \/ oexp x (cpred n) <o cnf_degree y) -> cnf_val x +o cnf_val y = cnf_val (cnf_nm y (cnf_ns x n)).
proof: Proof. move => ox ynz lnd ha hb. have od := (proj31_1 ha). have Ha i j: i <c (domain x) -> cardinalp j -> oexp x i <o oexp x j -> i <c j. move => idx cj lt1; case: (cleT_el cj (proj31_1 idx)) => // lji. move:(CNF_exponents_M (proj42 ox) (proj1 (proj44 ox)) lji idx). by move/(oltNge lt1). have nN := NS_lt_nat lnd (proj42 ox). have lt3:= (cle_ltT (cpred_le (CS_nat nN)) lnd). have kb: position_in_cnf x (cnf_degree y) = n. move:(position_in_cnf_prop ox od) => [ka kb kc]. have ck := (proj31 ka). case: (cleT_ell (proj31_1 lnd) ck); first exact. by move/kb => /proj1 /oleNgt;case. move => lkn;case: (equal_or_not n \0c) => nz. by move: lkn; rewrite nz => /clt0. case: hb => hb; first by case: nz. case: kc; first by move => kd; case: (cleNgt (proj1 lnd)); rewrite - kd. move => le1; move:(olt_leT hb le1) => eq2. move: (cpred_pr nN nz) =>[mN mv]. move:(Ha (cpred n) (position_in_cnf x (cnf_degree y)) lt3 ck eq2). by move/(cleSltP mN); rewrite - mv => /cleNgt; case. case: (inc_or_not (cnf_degree y) (domain (range x))) => hc. move/funI_P: hc =>[ p/(range_gP (proj41 ox)) [i idx iv] pv]. rewrite pv in ha hb; rewrite iv in ha hb. move/(NltP (proj42 ox)): idx => ilx. move: (Ha i n ilx (proj31_1 lnd) ha) => lin. case: (equal_or_not n \0c) => nz. by move: lin; rewrite nz => /clt0. move: (cpred_pr nN nz) =>[mN mv]. case: hb => // lt2. move:(Ha (cpred n) i lt3 (proj31_1 lin) lt2). by move/(cleSltP mN); rewrite - mv => /cleNgt; case. move: (cnf_sum_prop9 ox ynz hc); rewrite kb => <-. symmetry;apply:(cnf_sum_compat_prop ox (proj1 ynz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)