proposition: Lemma ordinals2_extc C1 C2 B1 B2 (E1 := cnext C1)(E2 := cnext C2) : infinite_c C1 -> infinite_c C2 -> iclosed_set B1 -> iclosed_set B2 -> ord_cofinal B1 E1 -> ord_cofinal B2 E2 -> C1 <=c C2 -> B1 = B2 \cap E1 -> agrees_on E1 (ordinalsE E1 B1) (ordinalsE E2 B2).
proof: Proof. move => ic1 ic2 cl1 cl2 cf1 cf2 c1c2 iv. move: (ordinals_set_normal1 ic1 cl1 cf1). move: (ordinals_set_normal1 ic2 cl2 cf2). rewrite -/E1 -/E2. set f1 := (ordinalsE E1 B1); set f2 := (ordinalsE E2 B2). move => [ax2 [[ff2 sf2 tf2] ninc2 cont2] im2]. move => [ax1 [[ff1 sf1 tf1] ninc1 cont1] im1]. have E1E2: sub E1 E2 by exact:(proj33 (cnext_pr6 c1c2)). have B1B2: sub B1 B2 by rewrite iv; apply: subsetI2l. have oe2: ordinalp E2 by move:(cnext_pr1 (proj1 ic2)) => [[]]. have oe1: ordinalp E1 by move:(cnext_pr1 (proj1 ic1)) => [[]]. have ob2: ordinal_set B2 by move => t /(proj1 cf2) /(Os_ordinal oe2). have ob1: ordinal_set B1 by move => t /B1B2 /ob2. move: (ordinals_set_iso ob1) => []. rewrite (ord_cofinal_p5 ic1 cf1). move: (ordinals_set_iso ob2) => []. rewrite (ord_cofinal_p5 ic2 cf2). set r1 := (fun x y => [/\ inc x B1, inc y B1 & x <=o y]). set r2 := (fun x y => [/\ inc x B2, inc y B2 & x <=o y]). rewrite -/E1 -/E2; move => ua2 ub2 ua1 ub1. move: (inverse_order_is ub2). set g2 := (Lf (ordinals r2) E2 B2); set g2' := inverse_fun g2 => ub3. have sr2: (substrate (ole_on B2)) = B2. by rewrite graph_on_sr // => a /ob2 /oleR. have sr1: (substrate (ole_on B1)) = B1. by rewrite graph_on_sr // => a /ob1 /oleR. move: (proj43 ub3); rewrite sr2 ordinal_o_sr => bg2. have sg2: source g2' = B2 by move: bg2 => [_ fb _]. have sa: forall x, inc x E1 -> inc (Vf g2' (ordinals r1 x)) E2. move => x /ua1 /B1B2 xsf; move: bg2 => [[[fa _] _] _ fc]; Wtac. set g3 := Lf (fun x => (Vf g2' (ordinals r1 x))) E1 E2. have isoc: order_morphism g3 (ordinal_o E1) (ordinal_o E2). move: ub1 ub3 => [pa _ _ pb] [_ pc _ pd]. split => //. by rewrite !ordinal_o_sr /g3; hnf; saw; apply:lf_function. hnf;rewrite /g3; aw => x y xe1 ye1; rewrite !LfV//. move: (pb x y);aw; rewrite !LfV// => h; move: (h xe1 ye1). set x' := (ordinals r1 x); set y' := (ordinals r1 y) => hh. have x'b2: inc x' B2 by apply/B1B2 /ua1. have y'b2: inc y' B2 by apply/B1B2 /ua1. move:(pd x' y'); rewrite sg2 => h'; move: (h' x'b2 y'b2) => hh'. apply: (iff_trans hh). split => //. by move => /graph_on_P1 [_ _ ok]; apply /hh' /graph_on_P1. move/hh' /graph_on_P1 => [_ _ ok]; apply /graph_on_P1. by split => //; apply:ua1. set g4 := Lf id E1 E2. have isod : order_morphism g4 (ordinal_o E1) (ordinal_o E2). move: isoc => [pa pb _ _]; split => //. rewrite !ordinal_o_sr /g4; hnf; saw; apply: lf_function => //. hnf;rewrite /g4; aw => x y xe1 ye1; rewrite !LfV//; split => //. move => /graph_on_P1 [_ _ ok]; apply /graph_on_P1. by split => //; apply:E1E2. by move /graph_on_P1 => [_ _ ok]; apply /graph_on_P1. have wo2: worder (ordinal_o E2) by apply: ordinal_o_wor. have wo1: worder (ordinal_o E1) by apply: ordinal_o_wor. have s1: segmentp (ordinal_o E2) (Imf g3). move: isoc=> [ _ _ [fg3 sg3 tg3] _]. split. by move => t /(Imf_P fg3); rewrite - tg3; move => [ x xe1 ->]; Wtac. move => x y /(Imf_P fg3) [x1 x1s ->] l2. have xe1: inc x1 E1 by move:x1s; rewrite sg3 ordinal_o_sr. move /ordo_leP: (l2) => [ye2 gx ll]; apply /(Imf_P fg3). move: ub2 => [_ _ [bg sg tg2] h2]; move: (h2 y (Vf g3 x1)); aw. rewrite LfV// => h3. move /(h3 ye2 gx): l2. have inc1: inc (ordinals r1 x1) B1 by apply :ua1. have eq2: (ordinals r2 (Vf g3 x1)) = ordinals r1 x1. transitivity (Vf g2 (Vf g3 x1)); first by rewrite /g2 LfV. by rewrite /g3 LfV //;apply: inverse_V => //; rewrite tg2 sr2; apply /B1B2. rewrite LfV // eq2; move /graph_on_P1=> [sa1 sb1 sc1]. move: ub1=> [_ _ [bg1 sg1 tg1] _]. have y'b1: inc (ordinals r2 y) (target (Lf (ordinals r1) E1 B1)). rewrite tg1 sr1 iv; apply /setI2_P; split => //. move: (proj1 cf1 _ inc1) => /(oltP oe1) lt2. apply /(oltP oe1); exact:ole_ltT sc1 lt2. have eq3: (ordinals r2 y) = Vf g2 y by rewrite /g2 LfV. move: (proj2 (proj2 bg1) _ y'b1) => [z]; rewrite lf_source => ze1. rewrite LfV// => zv; rewrite /g3; aw; exists z => //; rewrite LfV//. by rewrite - zv eq3 inverse_V2 // sg ordinal_o_sr. have s2:segmentp (ordinal_o E2) (Imf g4). hnf;rewrite/g4 - canonical_injectionE (ci_range E1E2) ordinal_o_sr. split => // x y /(oltP oe1) xe1 /graph_on_P1 [/(oltP oe2) ye2 _ xy]. apply/(oltP oe1); exact:(ole_ltT (And3 (proj31_1 ye2) (proj31_1 xe1) xy) xe1). move: (isomorphism_worder_unique wo1 wo2 s1 s2 isoc isod) => g3g4. hnf; rewrite sf1 sf2; split => // x xe1. have xe2 := (E1E2 _ xe1). rewrite /f1 /f2 /ordinalsE; aw; rewrite -/r1 -/r2. move: ub2 => [_ _ [bg _ tg] _]. have tg2: target g2 = B2 by move: tg; rewrite -/g2 sr2. move: (f_equal (Vf^~ x) g3g4); rewrite /g3 /g4 !LfV // => eq1. move: (f_equal (Vf g2) eq1); rewrite {2} /g2 LfV//. by rewrite inverse_V //; rewrite tg2; apply /B1B2/ ua1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)