proposition: Lemma oprod2_comm6 px n x py m y: CNFp_ax4 px n x -> CNFp_ax4 py m y -> oprod_comm x y -> oprod2_comm_P1 x y.
proof: Proof. move => h1 h2 h3. move:(h1)(h2) => [_ nN _ _] [_ mN _ _]. move:(NS_sum nN mN);set p := n +c m => pN. have aux: n +c m <=c p by rewrite /p; fprops. move: p pN aux => p pN aux. move: p pN px n x py m y h1 h2 h3 aux nN mN. have ores: forall px n x, CNFp_ax4 px n x -> ordinalp x. move=> px n x [[ax1 /proj33/proj1/OS_nat o1] nN _ ->]. exact: (OS_prod2 o1 (OS_CNFp1 ax1 (NS_succ nN))). have special: forall px n x, CNFp_ax4 px n x -> oprod2_comm_P1 x x. move=> px n x /ores h; move: (opowx1 h) => p1. exists x; exists \1c; exists \1c; split;fprops. apply: Nat_induction. move=> px n x py m y pa pb h1 h2 nN mN. move: (cle0 h2); rewrite -(osum2_2int nN mN) => nmz. move: (osum2_zero (OS_nat nN) (OS_nat mN) nmz) => [nz mz]. rewrite - mz in nz;move: (CNFp_ph pa pb h1) => [_ ok _]. move: (ok nz) => ok0; rewrite - ok0; apply: special pa. move=> sm smN hrec px n x py m y pa pb h1 h2 nN mN. wlog:px py n m x y pa pb h1 h2 nN mN / (m <=c n). move=> aux. case: (cleT_el (CS_nat mN) (CS_nat nN)). apply: aux pa pb h1 h2 nN mN. symmetry in h1; rewrite csumC in h2. move=> [lemn _]; move: (aux _ _ _ _ _ _ pb pa h1 h2 mN nN lemn). move => [z [xe [ye [oz xeN yeN eq1 e2]]]]. exists z; exists ye; exists xe; split => //. move: (CNFp_ph pa pb h1) => [_ pc pd]. move=> lenm; case: (equal_or_not m n) => dnm. symmetry in dnm;rewrite -(pc dnm); apply: (special _ _ _ pa). have ltnm: m <c n by split. move: (pd ltnm) => [pZ [p [z [pe xv h3 ltpn]]]]. have pN: natp p by move: ltpn => [lepn _];apply: (NS_le_nat lepn nN). move: (csum_Mlteq mN ltpn) => r1. move /(cltSleP smN): (clt_leT r1 h2) => le1. move: (hrec _ _ _ _ _ _ pe pb h3 le1 pN mN)=> xx. move: xx =>[t [xe [ye [oz xeN yeN eq1 e2]]]]. exists t; exists (xe +c ye); exists ye; split;fprops. have oxe: ordinalp xe by apply: OS_cardinal; fprops. have oye: ordinalp ye by apply: OS_cardinal; fprops. by rewrite xv eq1 e2 - (opow_sum oz oxe oye) (osum2_2int xeN yeN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)