proposition: Lemma multiple_interpolation_prop3 f1 f2 (Zb := Zo BQ (fun z => exists2 n, natp n & f1 n <q z)) (Za := Zo BQ (fun z => exists2 n, natp n & z <q f2 n)): (forall n, natp n -> f1 (csucc n) <q f1 n) -> (forall n, natp n -> f2 n <q f2 (csucc n)) -> (disjoint Za Zb) -> (Za \cup Zb = BQ) -> exists2 g, order_isomorphism g (induced_order BQ_order (BQ -s1 \0q)) BQ_order & Vfs g BQps = Zb.
proof: Proof. move => f1d f2i zdi zun. move:BQor_or BQor_sr=> or sr. have ha: sub BQps (substrate BQ_order) by rewrite sr; apply:BQps_sBQ. move:(multiple_interpolation_prop2 f1d). rewrite -/Zb; set g2 := Lf _ _ _; move => g2iso. pose f2' n := BQopp (f2 n). have pa':forall n, natp n -> f2' (csucc n) <q f2' n. by move => n nN; apply/ qlt_opp; apply: f2i. move:(multiple_interpolation_prop2 pa') => pa; clear pa'. move:(order_isomorphism_sincr pa); move:pa => []. set Zb' := Zo _ _; set g1 := Lf _ _ _. have hb': sub Zb' (substrate BQ_order) by rewrite sr; apply: Zo_S. rewrite (iorder_sr or ha) (iorder_sr or hb') => or1 or2 [bijg1 sg1 tg1] _ aux. pose g3 x := (BQopp (Vf g1 (BQopp x))). have g3i: forall x y, inc x BQms -> inc y BQms -> x <q y -> g3 x <q g3 y. move => x y /BQopp_negative1 xm /BQopp_negative1 ym lxy. have: glt (induced_order BQ_order BQps) (BQopp y) (BQopp x). by apply /iorder_gltP; split => //; apply/BQlt_P; apply/ qlt_opp. by move/aux =>/iorder_gltP [_ _] /BQlt_P => h; apply/ qlt_opp. have fg1 :=(proj1 (proj1 bijg1)). pose f x := Yo (x <q \0q) (g3 x) (Vf g2 x). have ra: forall x, inc x BQms -> inc (g3 x) Za. move => x /BQopp_negative1 ;rewrite - sg1 => /(Vf_target fg1). rewrite tg1 => /Zo_P [vq [n na nb]]; apply/Zo_P; split; first by apply: QSo. by exists n => //; move/ qlt_opp: nb; rewrite (BQopp_K (proj31_1(f2i _ na))). have rb: forall x, inc x BQms -> inc (f x) Za. by move => x xp;move / qgt0xP:(xp) => xq; rewrite /f; Ytac0; apply: ra. move:(order_isomorphism_sincr g2iso); move:g2iso => []. have hc: sub Zb (substrate BQ_order) by rewrite sr; apply: Zo_S. rewrite (iorder_sr or ha) (iorder_sr or hc) => _ or3 [bijg2 sg2 tg2] _ aux2. have fg2:=(proj1 (proj1 bijg2)). have g2i: forall x y, inc x BQps -> inc y BQps -> x <q y -> Vf g2 x <q Vf g2 y. move => x y xs ys lxy. have: glt (induced_order BQ_order BQps) x y. by apply /iorder_gltP; split => //; apply/BQlt_P. by move/aux2 =>/iorder_gltP [_ _] /BQlt_P => h. clear aux aux2. have xpnz: forall x, inc x BQps -> ~ (x <q \0q). move => x xp / qgt0xP xn; case:(BQ_di_neg_spos xn xp). have rc: forall x, inc x BQps -> inc (f x) Zb. move=> x xp; rewrite - tg2 /f (Y_false (xpnz _ xp)); Wtac. have s1: sub BQps (BQ -s1 \0q). by move => t /BQps_iP [/BQp_sBQ tq tnz]; apply/setC1_P. have rd: forall x, inc x (BQ -s1 \0q) -> inc (f x) BQ. move => x /setC1_P [/BQ_i1P xq xnz]. case: xq => //; [move/ rc | move/rb]; apply:Zo_S. have re1:forall y, inc y Zb -> exists2 x, inc x BQps & y = f x. move => y; rewrite - tg2 => /(proj2 (proj2 bijg2)). rewrite sg2; move => [x xi ->]; exists x => //; rewrite /f; Ytac h3 => //. move / qgt0xP: h3 => h4; case: (BQ_di_neg_spos h4 xi). have re:forall y,ratp y -> exists2 x, inc x (BQ -s1 \0q) & y = f x. rewrite /ratp - {1} zun => y /setU2_P; case;last first. by move/re1 => [x xa ->]; exists x => //;apply: s1. move /Zo_P => [yb [n na nb]]. have: inc (BQopp y) Zb'. apply/Zo_i; [ by apply: QSo | by exists n => //; move/ qlt_opp: nb]. rewrite - tg1 => /(proj2 (proj2 bijg1)); rewrite sg1;move => [x xa xb]. move:(BQopp_positive1 xa) => xn; move/ qgt0xP: (xn) => xn1. move:(xn1) (BQps_sBQ xa) => [/proj31 aa oxnz] xq. exists (BQopp x); first by apply/setC1_P. by rewrite /f (Y_true xn1) /g3 (BQopp_K xq) - xb (BQopp_K yb). have dip: forall x y, inc x Za -> inc y Zb ->x <q y. move => x y /Zo_P [xq [n na nb]] yb; move:(Zo_S yb) => yq. case: (qleT_el yq xq) => // lxy; move: (qle_ltT lxy nb) => l1. rewrite /disjoint in zdi; empty_tac1 y; apply/setI2_P; split => //. by apply /Zo_P; split => //; exists n. have finc: forall x y, inc x (BQ -s1 \0q) -> inc y (BQ -s1 \0q) -> x <q y -> f x <q f y. move => x y /setC1_P [/BQ_i1P xq xnz] /setC1_P [/BQ_i1P yq ynz] lxy. case: xq => // xp; case: yq => // yp. + by rewrite /f (Y_false (xpnz _ xp)) (Y_false (xpnz _ yp)); apply: g2i. + move/ qlt0xP: xp => h1;move/ qgt0xP: yp => h2. by case: (proj2 (qlt_ltT h2 (qlt_ltT h1 lxy))). + exact: (dip _ _ (rb _ xp) (rc _ yp)). + move/ qgt0xP: (xp) => h1;move/ qgt0xP: (yp) => h2. by rewrite /f; Ytac0; Ytac0; apply: g3i. set g := Lf f (BQ -s1 \0q) BQ. have bg: bijection g. apply: lf_bijective => // x y xp yp sf. move /setC1_P:(xp) => [xq _]; move /setC1_P:(yp) => [yq _]. case: (qleT_ell xq yq) => //; first by case/(finc _ _ xp yp). move/(finc _ _ yp xp) => [_ /nesym] //. have img: Vfs g BQps = Zb. have fg := (proj1 (proj1 bg)). have sg: sub BQps (source g). rewrite /g;aw;trivial => t /BQps_iP [ta tb];apply/setC1_P. set_extens x. move/(Vf_image_P fg sg) => [u up ->]; rewrite /g LfV//; first by apply: rc. by move: sg; rewrite /g; aw; apply. move/re1=> [y ya ->]; apply/(Vf_image_P fg sg);ex_tac;rewrite /g LfV//;fprops. exists g => //. have s2: sub (BQ -s1 \0q) (substrate BQ_order). by rewrite sr => t /setC1_P []. have to1:= (total_order_sub BQor_tor s2). have [or4 sr4]:= (iorder_osr or s2). apply:total_order_isomorphism => //; rewrite /g; aw; try ue. move => x y xs ys; rewrite !LfV// =>/iorder_gleP [_ _ /BQle_P lxy];apply/BQle_P. case: (equal_or_not x y) => eq; first by rewrite - eq; exact:(qleR(rd _ xs)). exact: (proj1 (finc _ _ xs ys (conj lxy eq))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)