proposition: Lemma cnf_sum_prop4 x k (x1 := cnf_val (cnf_nr x k)) (x2 := cnf_val (cnf_ns x (csucc k))) (x3 := oopow (oexp x k) *o (ocoef x k)): cnfp x -> k <c (domain x) -> [/\ ordinalp x1, ordinalp x2, ordinalp x3 & cnf_val x = x2 +o (x3 +o x1) ].
proof: Proof. move => ox lkd; rewrite /x1 /x2/x3. move:(NS_lt_nat lkd (proj42 ox)) => kN. have ha: csucc k <=c domain x by apply/cleSltP. split. - apply: (OS_cnf_val (cnfp_cnf_nr ox (proj1 lkd))). - apply:(OS_cnf_val (cnfp_cnf_ns ox ha)). - exact:(CNFq_p0 (proj1 (proj44 ox)) lkd). - rewrite -(cnf_sum_prop3 ox ha); apply: f_equal. rewrite /cnf_val /cnf_nr restr_d /CNFbvo /CNFbv (osum_fS _ kN) restr_d. apply: f_equal2. by rewrite/cantor_mon/oexp/ocoef LgV//; apply:Nsucc_i. apply: (osumf_exten kN) => i ilk. move/(NltP kN): (ilk) => is1. move:(proj33 (proj1 (cltS kN)) _ is1) => is2. by rewrite /cantor_mon/oexp/ocoef !LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)