proposition: Lemma cnf_sum_prop7 x y k: cnfp x -> cnfp_nz y -> k <c (domain x) -> oexp x k = cnf_degree y -> cnf_sum_compat x y.
proof: Proof. move => ox ynz lkd hk. move/(cnfpP): (ox) => ox'. move: (NS_lt_nat lkd (proj42 ox)) => kN. move/(cleSltP kN): (lkd) => lk1. have ox2:= cnfp_cnf_ns ox lk1. move/(NltP (proj42 ox)): (lkd) => kdx. move:(proj1 (proj33 (proj43 ox' _ kdx))) => cN. move: (cnf_nc_prop ynz cN) => [oy1 _ _ _ _]. have ovy := (OS_cnf_val (proj1 ynz)). rewrite /cnf_sum_compat (cnf_ncms_prop ox ynz lkd hk). rewrite (cnf_sum_prop1 oy1 ox2). move: (cnf_sum_prop4 ox lkd) => [ow ou ov ->]. rewrite - (osumA ou (OS_sum2 ov ow) ovy). apply: f_equal. rewrite (cnf_sum_prop6 ynz cN). move: ov; rewrite hk; move => ov. rewrite - (osumA ov ow ovy); apply: f_equal. move:(cnf_size_nz ynz)(cnf_size_nz_bis ynz). set m := cnf_size x; move => [mN dyv] hh. symmetry. apply: (ord_negl_p9 ox ynz (proj1 lkd)). move => i lik; rewrite - hk. apply:(CNF_exponents_sM (proj42 ox) (proj1 (proj44 ox)) lik lkd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)