proposition: Lemma finite_rems c: ordinalp c -> finite_set (Zo (osucc c) (fun b => exists2 a, ordinalp a & c = a +o b)).
proof: Proof. move => oc; set E := Zo _ _. pose p b a := ordinalp a /\ c = a +o b. pose Eb b := Zo (osucc c) (p b). have Pa: forall b, inc b E -> nonempty(Eb b). move => b/Zo_P [/(oleP oc) ha [a oa hc]]; exists a => //; apply:Zo_i => //. apply/(oleP oc); rewrite hc; apply:(osum_Mle0 oa (proj31 ha)). have Pb: forall b, ordinal_set (Eb b) by move => b a /Zo_hi []. pose f b := intersection (Eb b). have Pc: forall b, inc b E -> inc (f b) (Eb b). move => b /Pa h; apply:ordinal_setI => //. have CP: forall b, inc b E -> p b (f b) by move => b /Pc /Zo_hi. have ci: forall a b, inc a E -> inc b E -> a <o b -> f b <o f a. move => a b /CP [ofa s1] /CP [ofb s2] lab. case: (oleT_el ofa ofb) => // la. move: (osum_Meqlt lab ofa); rewrite - s1 => /oltNge; case. by move:(osum_Mleeq la (proj32_1 lab)); rewrite - s2. have ose: ordinal_set E by move => t /Zo_S /(Os_ordinal (OS_succ oc)). pose F := fun_image E f. have osf: ordinal_set F by move => t /funI_P [z /CP [osf _] -> ]. move:(wordering_ole_pr ose) => [ha hb]. move:(wordering_ole_pr osf) => [hc hd]. have he: forall i, inc i (substrate (ole_on E)) -> inc (f i) (substrate (ole_on F)). move =>i; rewrite hb hd => ie; apply/funI_P; ex_tac. have hf:forall i j, glt (ole_on E) i j -> glt (ole_on F) (f j) (f i). move => i j [/graph_on_P1 [ie je lij] nij]. move: (ci _ _ ie je (conj lij nij)) => [lfij nfij]. split => //; apply/graph_on_P1; split => //; apply/funI_P; first by exists j. by exists i. by move: (worder_decreasing_finite ha hc he hf); rewrite hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)