proposition: Lemma odegree_sum a b: ordinalp a -> ordinalp b -> odegree (a +o b) = omax (odegree a) (odegree b).
proof: Proof. move => oa ob. have deg0: odegree \0o = \0c by rewrite /odegree; Ytac0. case: (equal_or_not a \0o) => ap. by rewrite ap (osum0l ob) deg0 (omax_xy (ole0x (OS_degree ob))). case: (equal_or_not b \0o) => bp. by rewrite bp (osum0r oa) deg0 (omax_yx (ole0x (OS_degree oa))). case: (equal_or_not (a +o b) \0o) => abp. by case: (osum2_zero oa ob abp). move: (the_cnf_p0 oa); set x := the_cnf a; move => [ox xv]. move: (the_cnf_p0 ob); set y := the_cnf b; move => [oy yv]. rewrite /odegree (Y_false ap) (Y_false bp) (Y_false abp) -/x -/y. rewrite (cnf_osum oa ob) -/x -/y. have xz: x <> emptyset by move => xz; case: ap; rewrite -xv xz cnf_val0. have yz: y <> emptyset by move => yz; case: bp; rewrite -yv yz cnf_val0. move: (conj ox xz) (conj oy yz) => xnz ynz. move: (OS_cnf_degree xnz)(OS_cnf_degree ynz) => edx edy. case: (oleT_el edy edx) => ltd; last first. by rewrite (cnf_sum_small_deg xnz ynz ltd) (omax_xy (proj1 ltd)). rewrite (omax_yx ltd). symmetry; set d1 := cnf_degree x. have eq0:= (cnf_sum_range ox ynz). have os:= (conj (cnfp_sum ox oy) (cnf_sum_nz ox ynz)). have H := cnf_sum_rangeP ox ynz. apply: oleA. suff : exists2 p, inc p (range (cnf_sum x y)) & P p = d1. move => [p /(range_gP (proj41 (proj1 os))) [i idr iv] pv]. by move:(cnf_degree_greatest (proj1 os) idr); rewrite /oexp - iv pv. have Hb := (inc_V_range (proj41 ox) (cnf_size_nz_bis xnz)). case: (equal_or_not (cnf_degree y) d1) => eq1. exists (J d1 ((Vr x d1) +c (Vr y d1))); aw; trivial. by rewrite - eq1; apply /H; constructor 3. by exists (Vg x (cnf_size x)) => //; apply/H; constructor 2. move:(inc_V_range (proj41 (proj1 os)) (cnf_size_nz_bis os)). rewrite /cnf_degree/oexp;case /H. - move => [/(range_gP (proj41 oy)) [i idy ->] hv]. by move:(oleT (cnf_degree_greatest oy idy) ltd). - move => [/(range_gP (proj41 ox)) [i idx ->] hv]. exact:(cnf_degree_greatest ox idx). - by move ->; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)