proposition: Lemma oprod_neg_p1 x y: ordinalp x -> osuccp y -> x *o y = y -> x = \1o.
proof: Proof. move => ox yz eq1. have yp: \0c <o y by case:yz => [z oz ->]; apply: olt0S. have oy := proj32_1 yp. case: (ozero_dichot ox) => xp. by case: (proj2 yp); rewrite -eq1 xp oprod0l. move: (the_cnf_p0_nz yp); set b := the_cnf y; move=> [bnz yv]. move: (the_cnf_p0_nz xp); set a := the_cnf x; move=> [anz xv]. move:(ovaluation2_rev yz); rewrite /ovaluation -/b => vy0. move:(CNF_prod_pr6 anz bnz vy0); rewrite xv yv eq1 -yv=> eq2. move:(cnf_val_inj (proj1 bnz) (cnfp_prod_gen anz bnz) eq2) => eq3. move:(cnf_size_nz anz) (cnf_size_nz bnz). set n := cnf_size a; set m := cnf_size b; move => [nN nv][mN mv]. move:(f_equal domain eq3). have db: (domain b -c \1c) = m. by rewrite mv - (cpred_pr4 (CS_succ m)) (cpred_pr1 (CS_nat mN)). rewrite/cnf_prod_gen/cnf_nm /cnf_nck/cnf_shift_expo !Lgd. move => eq4; move:(eq4). rewrite mv nv - (cpred_pr4 (CS_succ m)) (cpred_pr1 (CS_nat mN)). rewrite (csum_Sn _ nN) - (csum_nS _ mN) -{1}(csum0l (CS_succ m)). move/(csum_eq2r (NS_succ mN) NS0 nN) => nz. move:(f_equal (Vg ^~\0c) eq3). have zdb:= proj1 (cnf_size_nz_ter bnz). move: (proj1 (cnf_size_nz_ter anz)). rewrite/cnf_prod_gen/cnf_nm /cnf_nck/cnf_shift_expo !Lgd - eq4. rewrite (LgV zdb) /cnf_m nv (Y_true (succ_positive _)) /cnf_c -/n - nz => i0z. rewrite (LgV i0z); Ytac0; move => eq5. move:(f_equal P eq5); aw; rewrite -/(oexp _ _)vy0 /cnf_degree -/n - nz => dz. move:(cnf_nat_prop anz (esym nz)(esym dz)) => [ /olt_omegaP eu ev]. rewrite ev in eu. move:(f_equal Q eq5); aw; rewrite -/(ocoef _ _) /cnf_lc -/n - nz. move/cnfpP: (proj1 bnz) => /proj43 hu. move:(proj33 (hu _ zdb)) => [q1 /proj2 /nesym q2]. rewrite - xv ev {1} /ocoef - {1} (cprod1l (CS_nat q1)). by move/(cprod_eq2r q1 NS1 eu q2) . Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)