proposition: Lemma cnf_sum_prop1 x y: cnfp x -> cnfp y -> cnf_val (cnf_nm x y) = (cnf_val y) +o (cnf_val x).
proof: Proof. move => ox oy. have nN := proj42 ox. have mN := proj42 oy. have nmN := (NS_sum nN mN). rewrite /cnf_val /CNFbvo /CNFbv /cnf_nm Lgd. set A := cantor_mon _ _ _. set B := cantor_mon _ _ _. set C := cantor_mon _ _ _. have propA t: t <c domain y -> A (t +c domain x) = B t. move => tdy; rewrite /A/B/cantor_mon /oexp/ocoef. move:(NS_lt_nat tdy mN) => tN. have qc:inc (t +c domain x) (domain x +c domain y). by apply/(NltP nmN ); rewrite csumC; apply:csum_Meqlt. move:(cleNgt(csum_Mle0 t (CS_nat nN))) => qd. by rewrite LgV// /cnf_m (Y_false qd) (cdiff_pr1 tN nN). have propB t : t <c domain x -> A t = C t. move => tdy; rewrite /A/C/cantor_mon/oexp/ocoef/cnf_m. have qc: inc t (domain x +c domain y). apply/(NltP nmN); apply: (clt_leT tdy). apply:(csum_M0le _ (CS_nat nN)). by rewrite LgV//; Ytac0. have propC: ord_below A (domain x +c domain y). move => t ts. move:(NS_lt_nat ts nmN) => tN. case: (NleT_el nN tN). move => le1; move: (cdiff_pr le1); set j := _ -c _ => ea. have jdx: j <c domain y. by apply:cdiff_Mlt => //; rewrite csumC. rewrite - ea csumC (propA _ jdx). exact:(CNFq_p0 (proj1 (proj44 oy)) jdx). move => tdx; rewrite (propB _ tdx). exact:(CNFq_p0 (proj1 (proj44 ox)) tdx). rewrite (osum_fA nN mN propC). apply: f_equal2. by apply: (osumf_exten mN) => t tn /=; apply: propA. by apply: (osumf_exten nN) => t tn /=;apply: propB. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)