proposition: Lemma big_ofs (p:= fun z => cnext (cardinal z)) (osup := fun f => \osup (fun_image (domain f) (fun z => (p (Vg f z))))) (osupp:= fun f => Yo (domain f = \0o) \0o (osup f)) (f:= transdef_ord osupp): [/\ normal_ofs f, f \0o = \0o, (forall x, ordinalp x -> f (osucc x) = p (f x))& forall C, infinite_c C -> exists x, inc x (cnext C) /\ ~ (inc (f x) (cnext C)) ].
proof: Proof. have sa: (forall x, ordinalp x -> x <o p x). move => x ox; rewrite /p. have pc: cardinalp (cardinal x) by fprops. have pa: cardinalp (cnext (cardinal x)) by apply: CS_cnext. apply /(oltP (proj1 pa)); apply /(cnextP pc); split; fprops. have sb: (forall x y, x <=o y -> p x <=o p y). move => x y xy; rewrite /p. have h := (ocle1 xy). by apply:ocle; apply:cnext_pr6. move: (normal_ofs_existence sa sb OS0). rewrite -/osup -/osupp -/f. move => [pa pb pc]; split => //. move => c ic; exists (osucc c). have cc:= (proj1 ic). have oc:= (proj1 cc). have cs:= (CS_cnext cc). have oso:=(OS_succ oc). split. have os1 := OS1. apply /(cnextP cc); split => //. rewrite - osucc_pr // osum_cardinal // (card_card cc) csum_inf //. fprops. rewrite (card_card CS1); apply: cle_fin_inf; fprops. have eq1: (f (osucc c)) = p (f c) by apply: pc. move /(cnextP cc)=> [sc sd]. have se: c <=o (f c) by apply: (osi_gex (proj1 pa) oc). have: p c <=o p (f c) by apply: sb. move /ocle1; rewrite - eq1 /p (card_card cc). rewrite (card_card cs) => h. exact: (cleNgt (cleT h sd) (cnext_pr2 cc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)