proposition: Lemma oprod_neg_p2 x y : \0o <o x -> limit_ordinal y -> (x *o y = y <-> odegree x <<o ovaluation y).
proof: Proof. move => xp ly. move: (ovaluation6 (limit_pos ly)) => [z sz yv]. have od:=(OS_degree (proj32_1 xp)). have ov:=(OS_valuation (limit_pos ly)). have oz: ordinalp z by case sz => [t /OS_succ ost ->]. move:(OS_pow OS_omega ov) (OS_pow OS_omega od) => oov ood. rewrite (CNF_prod_pr3 xp ly) {1 2} yv (oprodA ood oov oz). rewrite - (opow_sum OS_omega od ov); split => hyp; last by rewrite hyp. exact: (proj1 (ovaluation7 (OS_sum2 od ov) ov sz sz hyp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)