proposition: Lemma non_succ_ord_enum: (oprod2 omega0) =1o ordinalsf (fun x => ordinalp x /\ ~ (osuccp x)).
proof: Proof. set p := (fun x => ordinalp x /\ ~ (osuccp x)). have p0: forall x, p x -> x = \0o \/ limit_ordinal x. by move => x [/ordinal_limA h pa]; case: h; fprops. have p1: forall x, p x -> exists2 y, ordinalp y & x = omega0 *o y. move => x px; move: (px) => [ox _]; case: (p0 _ px). by move => ->; exists \0o; fprops; rewrite oprod0r. by move /(limit_ordinal_P4 ox) => [y [[_ oy _] _] yp]; exists y. have p2: forall x, limit_ordinal x -> p x. move => x lx; split; [exact: (proj31 lx) | exact:(limit_nonsucc' lx)]. have pz: p \0o by split; fprops; move => [n on ns]; by case:(@osucc_nz n). have p3: forall x, ordinalp x -> p (omega0 *o x). move => x ox; case: (ozero_dichot ox); first by move => ->;rewrite oprod0r. by move => xz; apply: p2; apply /limit_ordinal_P4; fprops; exists x. have opp: ordinal_prop p by move => x []. have p4 :(iclosed_proper p). split; first split => // F fl nef. have os: ordinal_set F by move => x /fl []. case: (ord_sup_inVlimit os nef); [by move => /fl | apply: p2]. apply:unbounded_non_coll => // x ox; exists(omega0 *o x); last by apply: p3. exact: (oprod_M1le olt_0omega ox). move:olt_0omega OS_omega => oo odo. apply:(normal_ofs_uniqueness (p:= fun z => z +o omega0)). - apply: (oprod_normal oo). - by apply: (ordinals_col_p2 p4). - by move => x ox; rewrite oprod2_succ. - move => x /(iclosed_col_fs p4). set u := ordinalsf p x; set v := ordinalsf p (osucc x). move => [uv pu pv h]; move: uv h; move/p1:pu => [a oa ->]. move/p1:pv => [b ob ->] /(oprod_Meqltr oa ob odo) => lab h. rewrite - (oprod2_succ odo oa); ex_middle bad. have ra := (oprod_Meqlt (oltS oa) oo). have rb := (p3 _ (OS_succ oa)). move: (oprod_Meqltr ob (OS_succ oa) odo (conj (h _ rb ra) bad)). by move /oltSleP => /(oltNge lab). - move: (iclosed_col_f0 p4); set u := ordinalsf p \0o. by rewrite oprod0r; move => [_ h]; move: (h _ pz) => /ole0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)