proposition: Lemma osum2_commutes a b: ordinalp a -> ordinalp b -> ((a +o b = b +o a) <-> (exists c n m, [/\ ordinalp c, natp n, natp m, a = c *o n & b = c *o m])).
proof: Proof. move=> oa ob; split; last first. move=> [c [n [m [oc nN mN av bv]]]]. have on: ordinalp n by apply: OS_cardinal; fprops. have om: ordinalp m by apply: OS_cardinal; fprops. rewrite av bv - (oprodD on om oc) - (oprodD om on oc). by rewrite (osum2_2int nN mN)(osum2_2int mN nN) csumC. move=> hc. case: (ozero_dichot oa) => az. exists b, \0c, \1c;split;fprops. by rewrite az (oprod0r). by rewrite (oprod1r ob). case: (ozero_dichot ob) => bz. exists a, \1c, \0c;split;fprops. by rewrite (oprod1r oa). by rewrite bz (oprod0r). case: (oleT_ell (OS_degree oa) (OS_degree ob)); last first => cab. case: (nesym (proj2 bz)); apply:(osum2_a_ab oa ob). rewrite hc;apply: (ord_negl_p7 bz az cab). case: (nesym (proj2 az)); apply:(osum2_a_ab ob oa). rewrite - hc;apply: (ord_negl_p7 az bz cab). move: (the_cnf_p0_nz az) => [axa av]. move: (the_cnf_p0_nz bz) => [axb bv]. move:(cnf_size_nz axa) (cnf_size_nz axb) cab. rewrite (odegree_of_nz (nesym (proj2 az))) (odegree_of_nz (nesym (proj2 bz))). set x := the_cnf a; set y := the_cnf b. set sa := (cnf_size x); set sb := cnf_size y. move=> [ua ub][uc ud] sd. rewrite -/x in axa; rewrite -/y in axb. set s1:= cnf_nc y (cnf_lc x). set s2 := cnf_nc x (cnf_lc y). move: (posnat_lc axa) (posnat_lc axb) => p1 p2. move: (cnf_nc_prop axa (proj1 p2)) (cnf_nc_prop axb (proj1 p1)). rewrite -/s1 -/s2; move => [ra2 rb2 rc2 rd2 re2] [ra1 rb1 rc1 rd1 re1]. have s1s2: s1 = s2. apply:(cnf_val_inj ra1 ra2). rewrite - (CNF_sum_pr3 axa axb sd) - (CNF_sum_pr3 axb axa (esym sd)). by rewrite /x/y av bv hc. have dxdy: domain x = domain y by rewrite -rb1 - rb2 s1s2. set s3 := Lg (domain x) (cnf_c (Vg x) (cnf_size x) (J (cnf_degree x) \1c)). move: (nesym(proj2(succ_positive sa))); rewrite - ub => dxz. have oexp3 i: inc i (domain x) -> oexp s3 i = oexp x i. by move => h;rewrite/s3/oexp/cnf_c LgV//; Ytac lt1; aw;trivial; rewrite lt1. have aux: cnfp_nz s3. rewrite/s3;split; last by move/domain_set0_P;aw. move/cnfpP:(proj1 axa) => [qa qb qc qd]. apply/cnfpP; split ; aww. move => i idx;rewrite LgV// /cnf_c; Ytac w;fprops. split;aww;[exact:(OS_cnf_degree axa) | exact PN1]. move => i iN lin;move:(qd i iN lin) => r. move/(NltP qb):(clt_ltT (cltS iN) lin)=> idx. move/(NltP qb): lin=> lin. by rewrite -/s3 (oexp3 _ idx)(oexp3 _ lin). have ds3: domain s3 = domain x by rewrite /s3 Lgd. have ss3: cnf_size s3 = cnf_size x by rewrite /cnf_size ds3. move:(cnf_size_nz_bis axa) => qq. have lcs3: cnf_lc s3 = \1c. by rewrite/s3/cnf_lc/ocoef ss3/cnf_c LgV//; Ytac0; aw. have dgcs3: cnf_degree s3 = cnf_degree x. by rewrite /cnf_degree ss3; apply: oexp3. have vs3 i: inc i (domain x) -> i <> cnf_size x -> Vg x i = Vg s3 i. by move => ha hb; rewrite/s3 LgV// /cnf_c; Ytac0. have eqx: x = (cnf_nck s3 (cnf_lc x)). move/cnfpP:(proj1 axa) => [qa _ qc _]. rewrite /cnf_nck dgcs3 lcs3 ds3 ss3(cprod1l (CS_nat(proj1 p1))). apply: fgraph_exten; aww => i idx;rewrite LgV//. rewrite /cnf_c; Ytac lt1; last by apply:vs3. by rewrite - (proj31 (qc i idx)) lt1. have eqy: y = (cnf_nck s3 (cnf_lc y)). rewrite /cnf_nck dgcs3 lcs3 ds3 ss3 (cprod1l (CS_nat(proj1 p2))). move/cnfpP:(proj1 axb) => [qa _ qc _]. apply: fgraph_exten; aww. rewrite dxdy => i idy;rewrite LgV // /cnf_c; Ytac lt1. have ->: cnf_degree x = cnf_degree y by rewrite/cnf_degree sd. by rewrite - (proj31 (qc i idy)) lt1 /cnf_size dxdy. move: (idy); rewrite - dxdy => idx. rewrite -(vs3 _ idx lt1). move: (f_equal (Vg ^~ i) s1s2); rewrite/s1/s2/cnf_nc/cnf_c !LgV//. by rewrite{1}/cnf_size -dxdy -/(cnf_size x); Ytac0; Ytac0. exists (cnf_val s3), (cnf_lc x),(cnf_lc y). split. - exact: (OS_cnf_val (proj1 aux)). - exact: (proj1 p1). - exact: (proj1 p2). - by rewrite (CNF_prod_pr1 aux p1) - av - eqx. - by rewrite (CNF_prod_pr1 aux p2) -bv - eqy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)