proposition: Lemma CNFp_ph px n py m x y (pz1 := CNF_npec px py n (csucc m)) (pz2 := CNF_npec py px m (csucc n)): CNFp_ax4 px n x -> CNFp_ax4 py m y -> oprod_comm x y -> [/\ (same_below pz1 pz2 (csucc n +c csucc m)), ( n = m -> x = y) & ( m <c n -> exists pz p z, [/\ CNFp_ax4 pz p z, x = z *o y, z *o y = y *o z & p <c n])].
proof: Proof. move=> [ ax nN exn xv] [ ay mN eym yv]. move:(NS_succ mN)(NS_succ nN) => smN snN. have sc1:= (csumC (csucc m)(csucc n)). have eq0:= (erefl(csucc n +c csucc m)). move: (CNFp_pg ax ay nN smN) (CNFp_pg ay ax mN snN). rewrite -{1} xv -{1} yv; move => [at1 eq1]. rewrite -{1} xv -{1} yv; move => [at2 eq2]. rewrite /oprod_comm eq1 eq2; clear eq1 eq2. move: (CNFp_unique at1 at2 (NS_sum snN smN) (NS_sum smN snN)); rewrite /CNFpv. set z1 := CNFpv1 _ _; set z2 := CNFpv1 _ _. rewrite /CNF_npec sc1 (Y_true eq0) (Y_true eq0) exn eym oopow0. move:(proj33(proj2 ax)) (proj33 (proj2 ay)) => pnu pnv. move: (OS_nat (proj1 pnu))(OS_nat (proj1 pnv)) => oq1 oq2. rewrite (oprod1l oq1) (oprod1l oq2). rewrite -/(CNF_npec px py _ _) - {2 3}sc1 -/(CNF_npec py px _ _) -/pz1 -/pz2. move => eq1 eq3; move: (proj2 (eq1 eq3)) => me; clear eq1 eq3. move:(true_below_rec (NS_sum snN smN) me) => [me1 me2]. split; first exact. move => enm; rewrite - enm in oq2 me1 me2. rewrite xv yv - enm. apply: f_equal2. by move: me2; rewrite /pz1/pz2 /CNF_npec - enm;Ytac0;Ytac0; move ->. apply: (oprodf_exten snN) => i lt1; rewrite /cantor_pmon. suff: px i = py i by move ->. have ha:= (csum_Mlteq snN lt1). have iN:= (NS_lt_nat lt1 snN). have eq2:= (cdiff_pr1 iN snN). have l1 := (Nsum_Mle0 i nN). have [hb1 hb2]: n <c i +c (csucc n). by rewrite (csum_nS _ nN);apply/(cltSleP((NS_sum iN nN))). move: (cleNgt hb1) => hb3. move: (me1 _ ha); move:(proj2 ha)=> hb. by rewrite/pz1/pz2/CNF_npec -enm; repeat Ytac0; rewrite eq2. move=> ltnm. move: me2; rewrite /pz1/pz2 /CNF_npec - sc1; Ytac0; Ytac0 => eqd. have snmnz: n -c m <> \0c by apply: (cdiff_nz ltnm). move: ltnm => [lenm nenm]. move: (cdiff_pr lenm) (NS_diff m nN) => snmp snmN. move: (cpred_pr snmN snmnz); set p := cpred (n -c m); move=> [pN pv1]. have spN: natp (csucc p) by fprops. set nm := (csucc n) +c (csucc m). have nmN:= NS_sum snN smN. have spm:csucc p +c csucc m = csucc n. by rewrite (csum_nS _ mN) csumC -pv1 snmp. have spm1: p +c csucc m = n. by rewrite (csum_nS _ mN) csumC - (csum_nS _ pN) -pv1. have nsm: (n -c csucc m) = p by apply: cdiff_pr2 => //. have pltn: p <c n by rewrite - spm1; apply: (csum_M0lt pN (@succ_nz m)). pose pz i:= Yo (i = csucc p) (px (csucc n)) (px (i +c (csucc m))). set z:= Q (px (csucc n)) *o CNFpv1 pz (csucc p). have axz: (CNFp_ax4 pz p z). move:(ax) =>[ a1 a2]. have aux: forall i, i<c csucc p -> i +c (csucc m) <c (csucc n). move => i isp. by move: (csum_Mlteq smN isp); rewrite spm. hnf; rewrite /z /pz; Ytac0. split; [ split; last by Ytac0 | exact | exact | reflexivity ]. move => i lip;move:(lip) => [_ h]; Ytac0; exact:(a1 _ (aux _ lip)). set eca:= CNF_npec pz py p (csucc m). have eqa: forall i, i <c (csucc n) -> eca i = px i. move => i ism; rewrite /eca. have ha:=(csum_Mlteq smN ism). move: (me1 _ ha); rewrite /pz /pz1/pz2 /CNF_npec spm sc1. rewrite 2!(Y_false (proj2 ha)) (Y_false (proj2 ism)). have iN:= (NS_lt_nat ism snN). have li1:= (Nsum_Mle0 i mN). move/(cltSleP (NS_sum iN mN)):li1. rewrite - (csum_nS _ mN) => - [ha4 ha5]. have ha7 := cleNgt ha4. have h3:= (proj2 (cltS pN)). repeat Ytac0. rewrite (cdiff_pr1 iN smN). case: (cleT_ell (proj31_1 ism) (CS_nat pN)) => cip. + by have ht:= (cleNgt lenm); rewrite cip spm1; repeat Ytac0. + move:(csum_Mlteq smN cip); rewrite spm1 => ha1. have ha6:= (proj2 (clt_leT cip (cleS pN))). by move:(proj2 cip)(proj2 ha1) => ha2 ha3; repeat Ytac0. + move:(csum_Mlteq smN cip); rewrite spm1; move => [/cleNgt hb1 hb2]. have ->: (i +c csucc m) -c csucc n = i -c csucc p. move/(cleSltP pN): cip => lt2. rewrite - {1} (cdiff_pr lt2) (csumC (csucc p)) - csumA spm. apply: (cdiff_pr1 (NS_diff (csucc p) iN) snN). move: cip => [/cleNgt ha8 ha9]. by repeat Ytac0. set ecb:=(CNF_npec py pz m (csucc p)). have eqb i: i <c (csucc n) -> px i = ecb i. move => iln; rewrite /ecb. have ha:=(clt_leT iln (csum_M0le (csucc m) (CS_succ n))). move: (me1 _ ha). rewrite /pz1/pz2/pz /CNF_npec sc1. move: (proj2 iln) (proj2 ha) => nin nin2. rewrite (csumC (csucc m)(csucc p)) spm; repeat Ytac0. case (equal_or_not i n) => ein. have h3:= (proj2 (cltS pN)); have h:= (cleNgt lenm). by move => _ ;rewrite ein nsm spm1; repeat Ytac0. have lin1: i <c n by split; [ apply/(cltSleP nN) | exact ]. repeat Ytac0. case : (cleT_ell (proj31_1 lin1) (CS_nat mN)) => cim. + by rewrite cim; repeat Ytac0. + by move: (proj2 cim) => hb; repeat Ytac0. + have smi: csucc m <=c i by move/(cleSltP mN): cim. move => _. rewrite (csumC (i -c csucc m)) (cdiff_pr smi). case: (equal_or_not (i -c csucc m) (csucc p)) => hu. by move: (cdiff_pr smi) nin; rewrite hu csumC spm => ->; case. move: cim => [/cleNgt hb hc]. by repeat Ytac0. move: (axz)=> [az1 az2 az3 cs4]. move: (proj2(CNFp_pg az1 ay pN smN)). have ->: CNFpv1 eca (csucc p +c csucc m) = CNFpv1 px (csucc n). rewrite spm; apply:(oprodf_exten snN) => i /eqa. by rewrite /cantor_pmon; move ->. rewrite - yv {1 3} /pz (Y_true (erefl _)) - [RHS] xv -/z => eqc. move:(proj2(CNFp_pg ay az1 mN spN)). have ->: CNFpv1 ecb (csucc m +c csucc p) = CNFpv1 px (csucc n). rewrite csumC spm; apply:(oprodf_exten snN) => i /eqb. by rewrite/cantor_pmon => ->. rewrite - cs4- {1} yv - eqd - xv => sc. by exists pz, p, z; rewrite eqc sc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)