proposition: Lemma oleading_coef_sum x y (a :=oleading_coef x) (b:=oleading_coef y): \0o <o x -> \0o <o y -> oleading_coef (x +o y) = Yo (odegree x <o odegree y) b (Yo (odegree y <o odegree x) a (a +c b)).
proof: Proof. move => xp yp. move: (the_cnf_p0_nz xp); set xc := the_cnf x; move => [xnz xv]. move: (the_cnf_p0_nz yp); set yc := the_cnf y; move => [ynz yv]. rewrite (odegree_of_pos xp) (odegree_of_pos yp). rewrite /a /b/oleading_coef(cnf_osum (proj32_1 xp) (proj32_1 yp)). rewrite -/xc -/yc -/(cnf_degree xc) -/(cnf_degree yc). move: (OS_cnf_degree xnz)(OS_cnf_degree ynz) => edx edy. case: (oleT_ell edx edy) => lt. - have ha: ~cnf_degree xc <o cnf_degree yc by rewrite lt;case. have hb: ~cnf_degree yc <o cnf_degree xc by rewrite lt;case. rewrite (Y_false ha) (Y_false hb). rewrite(cnf_ncms_prop_sd xnz ynz lt). rewrite/cnf_nc/cnf_c /cnf_size Lgd /ocoef LgV//; aw. by Ytac0; aw; trivial. move: (cnf_size_nz ynz) => [syN ->]. by rewrite cpred_pr1; fprops; apply:Nsucc_i. - by rewrite (cnf_sum_small_deg xnz ynz lt); Ytac0. - Ytac0; rewrite (Y_false (oleNgt (proj1 lt))). rewrite/ocoef; congr Q. set ms := Vg _ _; set mx := Vg _ _. move: (proj1 xnz)(proj1 ynz) => ox oy. have os := (cnfp_sum ox oy). have snz:= (conj os (cnf_sum_nz ox ynz)). have: inc mx (range (xc +f yc)). apply/(cnf_sum_rangeP ox ynz); constructor 2; split => //. move: (cnf_size_nz_bis xnz) => r1. apply/(range_gP (proj41 (proj1 xnz))); ex_tac. move/(range_gP (proj41 os)) => [i idx mv]. move:(cnf_size_nz snz); set s := cnf_size _; move => [ra rb]. move: idx; rewrite rb => /(NleP ra); case/cle_eqVlt => lis. by rewrite mv lis. move:(cnf_degree_greatest_bis os lis); rewrite /oexp - mv => lt1. move:(inc_V_range (proj41 os) (cnf_size_nz_bis snz)). move:(olt_ltT lt lt1) => lt2. case/(cnf_sum_rangeP ox ynz). + by move/proj2 => dd; case: (olt_ltT lt2 dd). + move => [ha _ ]. move/(range_gP (proj41 (proj1 xnz))): ha => [j jdx jv]. move:(cnf_size_nz xnz); set sx := cnf_size _; move => [wra wrb]. move: jdx; rewrite wrb => /(NleP wra);case/cle_eqVlt => liw //. by rewrite /ms jv liw. move:(oleNgt (proj1 (cnf_degree_greatest_bis (proj1 xnz) liw))). by rewrite /oexp - jv. + by move => ea; case: (proj2 lt2); move: (f_equal P ea); aw; move <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)