proposition: Lemma finite_rems2 f n b: natp n -> CNFr_ax f n -> ordinalp b -> ((exists2 a, ordinalp a & (CNFrv f n)= a +o b) <-> (exists2 k, k<=c n & b = CNFrv f k)).
proof: Proof. move => nN ax ob; split. move:n nN ax; apply:Nat_induction. move => ax [a oa] /esym; rewrite /CNFrv osum_f0. move/(osum2_zero oa ob) => [ _ ->]; exists \0c; fprops. by rewrite osum_f0. move => n nN Hrec axn [a oa bv]. case:(finite_rems_aux nN axn oa ob bv). move =>[ bc _ ]; exists (csucc n); fprops. move => [a' [oa' av asum]]. have h':exists2 a, ordinalp a & CNFrv f n = a +o b by exists a'. move: (Hrec (CNFr_ax_s nN axn) h') =>[k lkn kv]; exists k => //. exact:(cleT lkn (cleS nN)). move=> [k lkn ->]. have kN:= (NS_le_nat lkn nN). move:(cdiff_pr lkn); move: (NS_diff k nN); set m:= _ -c _=> mN dv. have ax2: ord_below (fun i => oopow (f i)) (k +c m). rewrite dv => i /(proj1 ax) ofi; apply: (OS_oopow ofi). rewrite/CNFrv - dv (osum_fA kN mN ax2). have op: ordinalp (CNFrv (fun z => f (z +c k)) m). apply:(OS_CNFr0 mN); split. by move => i /(csum_Meqlt kN); rewrite csumC dv => /(proj1 ax). move => i iN /(csum_Meqlt kN);rewrite csumC dv (csum_Sn _ iN) => lt. exact:(proj2 ax _ (NS_sum iN kN) lt). by exists (CNFrv (fun z => f (z +c k)) m). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)