proposition: Lemma oleading_coef_prod2 a b: \0o <o a -> omega0 <=o b -> oleading_coef (a *o b) = oleading_coef b.
proof: Proof. move => ap bi. move:(olt_leT olt_0omega bi) => bp. move : (odegree_infinite bi). clear bi. rewrite (odegree_of_nz (nesym(proj2 bp))). rewrite /oleading_coef /odegree. move:(the_cnf_p0_nz ap) (the_cnf_p0_nz bp). set x := the_cnf a; set y := the_cnf b. move=> [xnz <-][ynz <-] . rewrite -/(cnf_degree x) -/(cnf_degree y). have dxN := (proj42 (proj1 xnz)). move: (cnf_size_nz xnz)(cnf_size_nz ynz) => [sxN sxv] [syN syv]. have ody:= proj2(cnf_size_nz_ter ynz). move: (proj42(proj1 (proj44 (proj1 ynz))) \0c ody) => oox. have odx:=(OS_cnf_degree xnz). case: (ozero_dichot oox) => cz. rewrite (CNF_prod_pr6 xnz ynz cz). rewrite (proj43 (cnf_and_val_pb (cnfp_prod_gen xnz ynz))). rewrite /cnf_prod_gen /cnf_ns. have ->: (domain y -c \1c) = cnf_size y. by rewrite syv - cpred_pr4; fprops; rewrite cpred_pr2. set d1 := (domain x +c (cnf_size y)). have eq1: d1 = csucc ((cnf_size x) +c (cnf_size y)). by rewrite - (csum_Sn _ sxN) - sxv. have d1N: natp d1 by apply:(NS_sum dxN syN). have eq2: cpred d1 = (cnf_size x +c cnf_size y). rewrite eq1 cpred_pr2; fprops. have idd: inc (cpred d1) d1 by rewrite eq2 eq1; apply:Nsucc_i; fprops. rewrite/ cnf_prod_gen {1}/ocoef /cnf_size /cnf_nm Lgd. rewrite /cnf_nck /cnf_shift_expo /cnf_ns !Lgd -/d1. rewrite !LgV //eq2 /cnf_m; Ytac lt1. move/proj2; case. move/(NltP dxN):(lt1)=> lt2. move: lt1; rewrite sxv => /(cltSleP sxN). move: (Nsucc_i sxN)=> i3. rewrite -{2}(csum0r (CS_nat sxN)) => /(csum_le2l sxN syN NS0) /cle0 sy0. by rewrite /cnf_degree sy0 cz. case:(NleT_el dxN (NS_sum sxN syN)) => //; rewrite sxv. rewrite {1} (csucc_pr4 (CS_nat sxN)) => /(csum_le2l sxN NS1 syN) /cge1P. move => /proj2/nesym snz. move:(cpred_pr syN snz); set c := cpred _; move => [cN cv]. rewrite cv (csum_nS _ cN) -(csum_Sn _ sxN) csumC (cdiff_pr1 cN (NS_succ sxN)). rewrite syv (cpred_pr2 syN) /oexp/ocoef/cnf_s. have i3: inc c (cnf_size y) by rewrite cv; apply: Nsucc_i. by rewrite !LgV//;aw; rewrite - (csucc_pr4 (CS_nat cN)) - cv. move => _. rewrite (CNF_prod_pr5 xnz ynz cz). rewrite (proj43 (cnf_and_val_pb (cnfp_shift_expo (proj1 ynz) odx))). rewrite /ocoef/oexp/cnf_shift_expo /cnf_size Lgd LgV//; aw; trivial; by rewrite syv (cpred_pr2 syN); apply: Nsucc_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)