proposition: Lemma cofinality_succ x: ordinalp x -> \cf (osucc x) = \1o.
proof: Proof. move=> ox. have osx: ordinalp (osucc x) by fprops. have xsx: inc x (osucc x) by rewrite /osucc; fprops. move: (cofinality_rw osx) => [p1 _ p2]. apply: oleA ; last first. apply:oge1 => //; exact: (cofinality_n0 osx (@osucc_nz x)). apply: (p2 _ OS1). have ta: lf_axiom (fun _ : Set => x) \1o (osucc x) by move => t tc. have i01:inc \0o \1o by rewrite / \1o / \1c; fprops. exists ( Lf (fun z => x) \1o (osucc x)). split; first by saw; apply: lf_function. by move=> t ts; exists \0o => //; rewrite LfV //; apply /oleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)