proposition: Lemma CNFp_pg px n py m (pz := CNF_npec px py n m) (lx := Q (px (csucc n))) (ly := Q (py m)): CNFp_ax px (csucc n) -> CNFp_ax py m -> natp n -> natp m -> (CNFp_ax pz (csucc n +c m) /\ (lx *o (CNFpv1 px (csucc n))) *o (ly *o (CNFpv1 py m)) = lx *o CNFpv1 pz (csucc n +c m)).
proof: Proof. move=> ax ay nN mN. move:(ax) (ay) => [p1 p2] [p1' p2']. have snN:= NS_succ nN. have ltnsn:=(cltS nN). have lenn:= cleR (proj32_1 ltnsn). have cnn:=(CS_nat nN). have axz: CNFp_ax pz (csucc n +c m). have aux: forall i, i <c csucc n +c m -> i <> n -> ~ i <c n -> (i -c (csucc n) <c m). move => i pa. case: (cleT_ell cnn (proj31_1 pa)) => //; first by move => ->. move => /(cleSltP nN) => ha _ _. rewrite csumC in pa; have hh:= (NS_sum mN snN). exact: (cdiff_Mlt mN (NS_lt_nat pa hh) ha pa). split; last by rewrite /pz /CNF_npec; Ytac0. move => i isn; rewrite /pz /CNF_npec. move: (proj2 isn) => ha; Ytac0; clear ha. Ytac h0. move:(p1 _ ltnsn)=> [qa qb qc]; split; aww. move:(proj33 p2') => qd. by rewrite (oprod2_2int (proj1 qc) (proj1 qd)); apply:PN_prod. Ytac h3; first exact: (p1 _ (clt_leT h3 (proj1 ltnsn))). exact: (p1' _ (aux _ isn h0 h3)). split; first by exact. have ax':= (proj1 ax). have ox:=(OS_CNFp1 ax' snN). have oy:=(OS_CNFp1 (proj1 ay) mN). move:(OS_nat (proj1(proj33 p2))) (OS_nat (proj1(proj33 p2'))) => ocx ocy. rewrite - (oprodA ocx ox (OS_prod2 ocy oy)) (oprodA ox ocy oy); apply: f_equal. rewrite (CNFp_A snN mN (proj1 axz)). apply: f_equal2; last first. apply: (oprodf_exten mN) => i im. rewrite /CNFp_value1/pz/cantor_pmon/CNF_npec. have iN:= (NS_lt_nat im mN). move: (proj2 (csum_Mlteq snN im));rewrite (csumC m). move:(csum_Mlteq nN (succ_positive i)). rewrite (csum0l cnn) (cdiff_pr1 iN snN) (csum_nS _ nN). rewrite - (csum_Sn _ iN); move => [sa sb] sc. by move:(cleNgt sa) => sa'; repeat Ytac0. have nn1: n <c (csucc n) +c m. rewrite (csum_Sn _ nN); apply /(cltSleP (NS_sum nN mN)). apply: (csum_M0le _ cnn). have nn2: ~(n = csucc n +c m) by move: (proj2 nn1). move: (axz) => [p7 p8]. move:(p7 _ nn1) => [ha hb hc]. move: (p1 _ ( ltnsn)) => [ha' hb' hc']. move: (OS_CNFp0 (proj1 ax) (cltS nN)). rewrite (CNFp_r _ nN)(CNFp_r _ nN). rewrite /cantor_pmon (CNFp_pr1 hb hc)(CNFp_pr1 hb' hc') => o2. rewrite -(oprodA (OS_CNFp1r ax' snN (proj1 ltnsn)) o2 ocy); apply: f_equal2. apply: (oprodf_exten nN) => i lin. rewrite / CNFp_value1 /pz/CNF_npec /cantor_pmon. move:(proj2 (clt_leT lin (proj1 nn1))) (proj2 lin) => lt1 ne1. by repeat Ytac0. move: (OS_nat (proj1 (proj33 p2'))) (OS_nat (proj1 hc')) => ory orx. rewrite /CNFp_value2/pz/CNF_npec;repeat Ytac0; aw. by rewrite (oprodA (OS_succ (OS_oopow (proj32_1 hb'))) orx ory). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)