proposition: Lemma finite_rems_aux f n a b: natp n -> CNFr_ax f (csucc n) -> ordinalp a -> ordinalp b -> CNFrv f (csucc n) = a +o b -> (CNFrv f (csucc n) = b /\ a <o oopow (f n)) \/ (exists a', [/\ ordinalp a', a = oopow (f n) +o a' & CNFrv f n = a' +o b ]).
proof: Proof. move => nN axn oa ob sab. move:(proj1 axn n (cltS nN)) => ofn. move: (OS_pow OS_omega ofn) => op1. have eq1:= (CNFr_rec f nN). have ops := (OS_CNFr0 nN (CNFr_ax_s nN axn)). case: (oleT_el op1 oa)=> lta; [right | left]. move:(odiff_pr lta); set a' := _ -o _; move => [oa' eq2]. exists a'; split => //. move: sab; rewrite eq1 eq2 - osumA //. by move/(osum2_simpl ops (OS_sum2 oa' ob) op1). split=>//;move:(ord_negl_opow lta ofn) => na. move:(ord_negl_sum oa (proj32_1 lta) ops na). by rewrite -eq1 sab => /(ord_neg_sum4 oa ob);rewrite/ord_negl - sab. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)