proposition: Lemma CNFr_exists x: ordinalp x -> exists f n, [/\ natp n, CNFr_ax f n & x = CNFrv f n].
proof: Proof. pose p := fun x => exists f n, [/\ natp n, CNFr_ax f n & x = CNFrv f n]. move:x; apply:(least_ordinal2) => y oy p2. case: (ozero_dichot oy) => yp. exists (@id Set), \0c; split; [ exact: NS0 | | by rewrite CNFr_p5 yp]. split => i; [ move /clt0; case | move => _ /clt0; case]. move: (CNFr_exists_aux yp) => [e1 [z [oe zly lt1 yv]]]. move:(p2 _ zly) => [f [n [nN p4 p5]]]. have snb:= (NS_succ nN). pose g z:= (Yo (z = n) e1 (f z)). have yv3: y = CNFrv g (csucc n). rewrite /CNFrv (osum_fS _ nN) /g yv; Ytac0; congr (osum2). by rewrite p5;apply: (osumf_exten nN) => i [_ lin]; Ytac0. exists g,(csucc n); split => //. split. move => i; rewrite /g; Ytac ein => //. by move/(cltSleP nN) => lin; apply:(proj1 p4). move => i iN h; rewrite /g. move/(cltSleP nN): h => sin. Ytac ein; first by move: (cltS nN); rewrite - {2} ein => /(cleNgt sin). Ytac sein; last by apply:(proj2 p4). move: (cltS iN); rewrite sein => lin. apply/oltSleP; apply/(opow_Mo_ltP (proj1 p4 _ lin) (OS_succ oe)). apply: (ole_ltT (CNFr_p3 nN p4 lin)). by rewrite - p5 (oopow_succ oe). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)