proposition: Lemma oprod_crit_aux n x (y := oopow (oopow n)): ordinalp n -> \1o <=o x -> x <o y -> x *o y = y.
proof: Proof. move => on x1 xy. move: OS_omega OS1 olt_1omega => oo o1 lt1o. have oy1:= OS_pow OS_omega on. have oy:= OS_pow OS_omega oy1. have xp: \0o <o x by apply/oge1P. rewrite (CNF_prod_pr3 xp (indecomp_limit2 (oopow_pos on))). have ox:= proj32 x1. have od:=(OS_degree ox). rewrite - (opow_sum OS_omega od oy1). rewrite (indecomp_prop1 (indecomp_prop4 on)) //. by apply: the_cnf_p6. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)