proposition: Theorem oprod2_comm x y: ordinalp x -> ordinalp y -> ((oprod_comm x y) <-> (x = \0o \/ y = \0o \/ (oprod2_comm_P4 x y \/ oprod2_comm_P4 y x) \/ (x <o omega0 /\ y <o omega0) \/ oprod2_comm_P1 x y)).
proof: Proof. move=> ox oy. split; last first. rewrite /oprod_comm. move => h; case: h; first by move=> ->; rewrite (oprod0r) (oprod0l). case; first by move=> ->; rewrite (oprod0r) (oprod0l). case; first by case ;[ apply: oprod2_comm3 | symmetry; apply: oprod2_comm3 ]. case. move => [/olt_omegaP xN /olt_omegaP yN]. by rewrite (oprod2_2int xN yN)(oprod2_2int yN xN) cprodC. move=> [c [n [m [oc nN mN -> ->]]]]. move:(OS_nat nN) (OS_nat mN) => on om. rewrite - (opow_sum oc on om) - (opow_sum oc om on). by rewrite (osum2_2int nN mN)(osum2_2int mN nN) csumC. move=> h. case: (ozero_dichot ox) => xnz; first by left. case: (ozero_dichot oy) => ynz; [by right;left | right; right]. case: (equal_or_not y \1c) => y1. by right;right;exists x, \1o, \0c;split;fprops; rewrite ?opowx1 // y1 opowx0. case: (equal_or_not x \1c) => x1. by right;right;exists y,\0c,\1c;split;fprops; rewrite ? opowx1 // x1 opowx0. move: (the_cnf_p0_nz xnz) (the_cnf_p0_nz ynz). set a := the_cnf x; set b := the_cnf y. move =>[anz av] [bnz bv]. have h1:oprod_comm (cnf_val a) (cnf_val b) by rewrite av bv. move:(cnf_size_nz anz) (cnf_size_nz bnz). set m := cnf_size a; set m' := cnf_size b; move => [mN mv][m'N m'v]. move: (proj42 (proj1(proj44 (proj1 anz)))) => ax0. move: (proj42 (proj1(proj44 (proj1 bnz)))) => ay0. have l0x:=(proj2 (cnf_size_nz_ter anz)). have l0y:=(proj2 (cnf_size_nz_ter bnz)). move: (ax0 _ l0x) (ay0 _ l0y) => oex0 oey0. case: (ozero_dichot oex0) => limX; last first. case: (ozero_dichot oey0) => limY; last first. by move: (oprod2_comm4 anz bnz limX limY h1); rewrite av bv; left. move:(oprod2_comm1 anz bnz limY limX h1);rewrite bv => h2; contradiction. case: (ozero_dichot oey0) => limY; last first. symmetry in h1. move: (oprod2_comm1 bnz anz limX limY h1); rewrite av => h2;contradiction. case: (equal_or_not (cnf_size a) \0c) => n1. move: (oprod2_comm5 anz bnz limX limY n1 h1); rewrite av bv. case => h2; [ by case: x1 | by right;left]. case: (equal_or_not (cnf_size b) \0c) => m1. symmetry in h1. move: (oprod2_comm5 bnz anz limY limX m1 h1); rewrite av bv. case => h2; [ by case: y1 |move: h2 => [q1 q2];by right;left; split]. right; right. move: (CNFp_exists xnz) => [px [n [ax2 nN xv2]]]. move: (CNFp_p4 ax2 nN) => [e''x [c''x [ax3 xv3 ex1 eqx2]]]. move: (proj44 (proj1 anz)); rewrite mv => ax1. move: xv3; rewrite - xv2 - {1} av /cnf_val mv => xv3. move: (CNFb_unique (NS_succ nN) (NS_succ mN) ax3 ax1 xv3) => [sa scx]. have mn:=(csucc_inj (CS_nat nN) (CS_nat mN) sa). rewrite mn in eqx2 scx xv2 ax2; clear sa mn xv3. move: (CNFp_exists ynz) => [py [n' [ay2 n'N yv2]]]. move: (CNFp_p4 ay2 n'N) => [e''y [c''y [ay3 yv3 ey1 eqy2]]]. move: yv3; rewrite - yv2 - {1} bv /cnf_val m'v => yv3. move: (proj44 (proj1 bnz)); rewrite m'v => ay1. move: (CNFb_unique (NS_succ n'N) (NS_succ m'N) ay3 ay1 yv3) => [sa scy]. have mn:=(csucc_inj (CS_nat n'N) (CS_nat m'N) sa). rewrite mn in eqy2 scy yv2 ay2; clear sa mn yv3. move: (proj2 (proj44 (proj1 anz)) _ l0x) => c1a. move: (proj2 (proj44 (proj1 bnz)) _ l0y) => c2a. move:(proj32_1 c1a) (proj32_1 c2a) => oc1 oc2. move: xv2 yv2; rewrite /CNFpv eqy2 eqx2. move: (scy _ (succ_positive m')) (scx _ (succ_positive m)) => [e1 e2][e3 e4]. rewrite e1 e2 e3 e4 limX limY. aw; rewrite oopow0 (oprod1l oc1) (oprod1l oc2) => xv4 yv4. have ax5: (CNFp_ax4 px (cpred m) x). move: (cpred_pr mN n1) => [qa qb]. by hnf; rewrite - qb eqx2 pr1_pair pr2_pair e3 e4 limX - xv4; split. have ay5: (CNFp_ax4 py (cpred m') y). move: (cpred_pr m'N m1) => [qa qb]. by hnf; rewrite - qb eqy2 pr1_pair pr2_pair e2 e1 limY - yv4; split. exact: (oprod2_comm6 ax5 ay5 h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)