proposition: Lemma opow_rec_def a b: \2o <=o a -> ordinalp b -> a ^o b = unionb (Lg b (fun x => fun_image( (a-s1 \0o)\times a ^o x) (fun p => (a^o x) *o (P p) +o (Q p)))) +s1 \0o.
proof: Proof. move => a2 ob. have oa:= proj32 a2. have ap:= (olt_leT olt_02 a2). have oab:= OS_pow oa ob. set_extens t => h; last first. apply /(oltP oab);case /setU1_P:h; last first. by move => ->; apply: opow_pos. move => /setUb_P; aw; move => [x xa]; rewrite LgV//. move/(oltP ob): xa => lxb. have ox:= (proj31_1 lxb). have oax:= (OS_pow oa ox). move /funI_P => [p /setX_P [pp /setC1_P [ua unz] /(oltP oax) vb] ->]. have ou:= (Os_ordinal oa ua). move:ua => /(oltP oa) /oleSltP ua. move:(osum_Meqlt vb (OS_prod2 oax ou)) => h; apply: (olt_leT h). rewrite - (oprod2_succ oax ou). move:(oprod_Meqle ua oax); rewrite - (opow_succ oa ox). move => h1; apply: (oleT h1); apply: opow_Meqle => //. by apply/oleSltP. have ot:= (Os_ordinal oab h). apply/setU1_P;case:(ozero_dichot ot);[ by right | move => tnz ; left]. move: (ord_ext_div_exists a2 tnz) => [x [y [z [ox oy oz [tv r1 r2 r3]]]]]. have aux: inc x b. apply /(oltP ob); case: (oleT_el ob ox) => // bx. move: (oleT (opow_Meqle ap bx) (oprod_Mle1 (proj32_1 r1) r3))=> l1. move: (oleT l1 (osum_Mle0 (proj32 l1) oz)); rewrite - tv => l2. by move /(oltP oab):h => /(oleNgt l2). apply/setUb_P; aw; exists x => //; rewrite LgV//. apply /funI_P; exists (J y z); aw; trivial;apply: setXp_i => //. apply /setC1_P; split; [ by apply/(oltP oa) | exact: nesym (proj2 r3)]. exact: (olt_i r1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)