proposition: Lemma non_zero_ord_enum: (osum2 \1o) =1o ordinalsf (fun x => \0o <o x).
proof: Proof. set p := (fun x => \0o <o x). have pa :(iclosed_proper p). split. split; first by move => x [] []. move => F hx [t tx]. have osf: ordinal_set F by move => x /hx [[] ]. move: (ord_sup_ub osf tx); apply: olt_leT; exact (hx _ tx). apply: unbounded_non_coll => x ox; exists (osucc x); first exact:(oleS ox). by apply:olt0S. apply:(normal_ofs_uniqueness (p:= fun z => z+o \1o)). - exact: (osum_normal OS1). - exact: (ordinals_col_p2 pa). - by move => x ox; rewrite - (osucc_pr ox) (osumA OS1 ox OS1). - move => x /(iclosed_col_fs pa). set u := ordinalsf p x; set v := ordinalsf p (osucc x). rewrite /p;move =>[/oleSltP uv [[_ ou _] _] _ h]. rewrite (osucc_pr ou); apply: oleA => //. apply: h; [by apply:olt0S | by apply:oltS]. - move: (iclosed_col_f0 pa); set u := ordinalsf p \0o. rewrite (osum0r OS1); move => [] /oge1P u1 h. exact: (oleA u1 (h _ olt_01)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)