proposition: Lemma finite_rems3 f n (c := (CNFrv f n)): natp n -> CNFr_ax f n -> cardinal (Zo (osucc c) (fun b => exists2 a, ordinalp a & c = a +o b)) = csucc n.
proof: Proof. move => nN ax; set E := Zo _ _. have smon k: k <=c n -> CNFrv f k <=o CNFrv f n. clear c E; move: n nN ax; apply: Nat_induction. move => ax /cle0 ->; exact:(oleR (OS_CNFr0 NS0 ax)). move => n nN Hrec ax; case /cle_eqVlt. by move ->; exact:(oleR (OS_CNFr0 (NS_succ nN) ax)). move/(cltSleP nN) => lkn. have le1 := (Hrec (CNFr_ax_s nN ax) lkn). have oo := (OS_pow OS_omega(proj1 ax n (cltS nN))). rewrite (CNFr_rec _ nN). exact: (oleT le1 (osum_M0le oo (proj32 le1))). have oc:=(OS_CNFr0 nN ax). have ->: E = fun_image (Nintc n) (CNFrv f). set_extens b. move => /Zo_P [/(oleP oc) /proj31 ob]. move /(finite_rems2 nN ax ob) => [k /(NintcP nN) kI ->]. apply/funI_P;ex_tac. move => /funI_P [k /(NintcP nN) kI ->]. move:(smon _ kI) => sm1. have sm: inc (CNFrv f k) (osucc c) by apply/(oleP oc). by apply:(Zo_i sm);apply/(finite_rems2 nN ax (proj31 sm1)); exists k. rewrite cardinal_fun_image ?(card_Nintc nN) //. have axr k: k<=c n -> CNFr_ax f k. move => lkn;split. by move => i lik; exact:(proj1 ax _ (clt_leT lik lkn)). move => i iN lik; exact:(proj2 ax _ iN (clt_leT lik lkn)). move => i j /(NintcP nN) lin /(NintcP nN) ljn /= sv. by case: (CNFr_unique (axr _ lin) (axr _ ljn) (NS_le_nat lin nN)(NS_le_nat ljn nN) sv). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)