proposition: Lemma multiple_interpolation_prop2 f (g := multiple_interpolation2 f) (Z := Zo BQ (fun z => exists2 n, natp n & f n <q z)): (forall n, natp n -> f (csucc n) <q f n) -> order_isomorphism (Lf g BQps Z) (induced_order BQ_order BQps) (induced_order BQ_order Z).
proof: Proof. move => finc. have Ha: forall i, natp i -> inc (f i) BQ by move => i /finc/proj32_1. have Hb: forall x, \1q <q x -> g x = (x +q (f \0c) -q \1q). move => x lt1;rewrite /g /multiple_interpolation2. have xp: inc x BQps by move/ qlt0xP: QpsS1 => h;apply / qlt0xP; BQo_tac. move/(BQinv_mon2 xp QpsS1): lt1 => sa. move: (QpsS_inv xp) => / qlt0xP [ip _]. have <-: \0z = (BQfloor (BQinv x)). by apply: (BQ_floorp2 (proj31_1 sa) ZS0);rewrite (BQsum_0l QS1) -BQinv_1. by rewrite / BZ_zero /BZ_of_nat; aw; Ytac0. have Hc: forall x, \1q <q x -> f \0c <q g x. have ha := (Ha _ NS0). move => x h; move:(proj32_1 h) => xq. rewrite (Hb _ h) /BQdiff (BQsum_AC xq ha (QSo QS1)). by rewrite BQsumC; apply/ (BQsum_Mps ha)/ qlt0xP /(qlt_diffP1 QS1 xq). have Hd: forall a, f \0c <q a -> exists2 x, \1q <q x & a = g x. move => a ap;move: (ap) => [[f0q aq _] _]. have ha: \1q <q (a +q \1q) -q f \0c. rewrite /BQdiff (BQsum_AC aq QS1 (QSo f0q)) BQsumC; apply/ (BQsum_Mps QS1). by apply / qlt0xP / qlt_diffP1. exists ( (a +q \1q) -q (f \0c)) => //. by rewrite (Hb _ ha) (BQsum_diff1 f0q (QSs aq QS1))(BQdiff_sum1 QS1 aq). have He: forall x, \1q <q x -> inc (g x) Z. move => x /Hc h; apply/Zo_P;split; [ exact:(proj32_1 h) | exists \0c; fprops]. have Hf: forall x, \0q <q x -> x <=q \1q -> \1q <=q BQinv x. by move => x / qlt0xP ha hb; move/(BQinv_mon1 QpsS1 ha): hb; rewrite BQinv_1. have Hg: forall x, \0q <q x -> x <=q \1q -> \1z <=z BQfloor (BQinv x). move => x ha hb; move:(Hf _ ha hb) => hc. by rewrite - (BQfloor_Z ZS1); apply: BQfloor_M. pose xn x := (cpred (BZ_val (BQfloor (BQinv x)))). have xnp1: forall x, ratp x -> natp (xn x). by move => x xq; apply /NS_pred /BZ_valN/ZS_floor /QS_inv. have xnp2: forall x, \0q <q x -> x <=q \1q -> BQfloor (BQinv x) = BZ_of_nat(csucc (xn x)). move => x ha hb. move/zlt0xP: ZpsS1 => sb; move:(zlt_leT sb (Hg x ha hb)) =>/zlt0xP. rewrite /xn; set y := BQfloor (BQinv x) => sc. rewrite -(proj2 (cpred_pr (BZ_valN (BZps_sBZ sc)) (BZps_valnz sc))). by rewrite(BZp_hi_pr (BZps_sBZp sc)). have xnp3: forall x, \0q <q x -> x <=q \1q -> P (BQfloor (BQinv x)) = csucc (xn x). by move => x ha hb; rewrite (xnp2 x ha hb) BZ_of_nat_val. pose yk k := (BQinv (BQ_of_nat (csucc k))). have ykp0: forall k, natp k -> \0q <q (yk k). by move => k kN; apply / qlt0xP; apply: QpsS_inv; apply: BQpsS_fromN. have ykp1: forall n, natp n -> yk n <=q \1q. move => n nN. rewrite - BQinv_1; apply/(BQinv_mon1(BQpsS_fromN nN) QpsS1). apply /(qle_cN NS1 (NS_succ nN)). by rewrite - succ_zero;apply:cleSS; apply:cle0n. have ykp2: forall x, \0q <q x -> x <=q \1q -> yk (csucc (xn x)) <q x /\ x <=q yk (xn x). move => x pa pb; move: (proj32_1 pa)=> xq;move: (xnp1 _ xq) => nN. move: (xnp2 x pa pb) (QS_inv xq) => pc iq. move/ qlt0xP: (pa) => xp. move:(NS_succ nN) => snN. have ha:= (QpsS_inv (BQpsS_fromN nN)). have hb:= (QpsS_inv (BQpsS_fromN snN)). move:(BQ_floorp iq) => []; rewrite (BQsum_cZ (ZS_floor iq) ZS1) pc. rewrite (BZsum_cN snN NS1) - (Nsucc_rw snN) -/(BQ_of_nat _). rewrite - (BQinv_K (QS_of_nat snN)); move/(BQinv_mon1 ha xp) => le1. rewrite -/(BQ_of_nat _) - (BQinv_K (QS_of_nat (NS_succ snN))). by move/(BQinv_mon2 xp hb) => le2. have ykp4':forall a b, natp a -> natp b -> a <c b -> yk b <q yk a. move => a b aN bN lab. move:(BQpsS_fromN aN)(BQpsS_fromN bN) => ap bp. by apply/(BQinv_mon2 bp ap) /(qlt_cN (NS_succ aN) (NS_succ bN)) /cltSS. have ykp4:forall a b, natp a -> natp b -> a <=c b -> yk b <=q yk a. move => a b aN bN lab. move:(BQpsS_fromN aN)(BQpsS_fromN bN) => ap bp. by apply/(BQinv_mon1 bp ap)/(qle_cN (NS_succ aN) (NS_succ bN)) /cleSS. have ykp5: forall n x, natp n -> yk (csucc n) <q x /\ x <=q yk n -> [/\ \0q <q x, x <=q \1q & n = xn x]. move => n x nN [sa sb]. move / qlt0xP:(QpsS_inv (BQpsS_fromN (NS_succ nN))) => sc. move: (qlt_ltT sc sa) => sd; move:(qleT sb (ykp1 _ nN)) => se. split => //; move:(ykp2 _ sd se) => [sa' sb']. move:(qlt_leT sa sb') (qlt_leT sa' sb)(xnp1 _ (proj31 sb)) => lt1 lt2 xN. case:(NleT_ell nN xN) => //. move /(cleSltP nN) => /(ykp4 _ _ (NS_succ nN) xN) => h; BQo_tac. move /(cleSltP xN) => /(ykp4 _ _ (NS_succ xN) nN) => h; BQo_tac. have ykp6: forall n, natp n -> n = xn (yk n). move => n nN;move: (ykp4' _ _ nN (NS_succ nN) (cltS nN)) => ha. exact: (proj33 (ykp5 n (yk n) nN (conj ha (qleR (proj32_1 ha))))). have Hi: forall x, \0q <q x -> x <=q \1q -> g x = (simple_interpolation2 (csucc (xn x)) (f (csucc (xn x))) (f (xn x)) x). move => x ha hb; move: (xnp3 _ ha hb) => hc. rewrite /g/multiple_interpolation2 hc (Y_false (@succ_nz _)). by rewrite (cpred_pr1 (CS_nat (xnp1 _ (proj32_1 ha)))). have Hj: forall n, natp n -> g (yk n) = f n. move => n nN; rewrite (Hi _ (ykp0 _ nN) (ykp1 _ nN)) - (ykp6 _ nN). by move: (simple_interpolation2_pa nN (finc _ nN)) => [_ sa _ _]. have Hk: forall x, \0q <q x -> x <=q \1q -> (f (csucc (xn x)) <q g x /\ g x <=q f (xn x)). move => x pa pb; rewrite (Hi x pa pb). move: (xnp1 _ (proj32_1 pa)) => nN. move: (ykp2 x pa pb) => [lt1 lt2]. move:(simple_interpolation2_pa nN (finc _ nN)). set A := simple_interpolation2 _ _ _; rewrite -/(yk _ ) -/(yk _ ). move => [r1 r2 r3 _];rewrite - r1 - r2; split; first by exact:(r3 _ _ lt1). case: (equal_or_not x (yk (xn x))) => eq1. rewrite {1} eq1 r2; apply: (qleR (proj32_1(finc _ nN))). exact: (proj1 (r3 _ _ (conj lt2 eq1))). have ra: forall x, inc x BQps -> inc (g x) Z. move => x xp;move / qlt0xP: (xp) => ha; move:(BQps_sBQ xp) => xq. case: (qleT_el xq QS1) => hb; last by apply: He. move: (Hk _ ha hb) => [hc _]; apply: Zo_i; first exact:(proj32_1 hc). exists (csucc (xn x)) => //; apply: (NS_succ (xnp1 _ xq)). have lt01: \0q <q \1q by apply/ qlt0xP; exact:QpsS1. have rb: forall y, inc y Z -> exists2 x, inc x BQps & y = (g x). move => y /Zo_P [yq [m mN hm]]. case: (least_int_prop2 mN hm (p := fun t => f t <q y)). move/Hd => [x sa sb]; exists x => //; apply / qlt0xP; BQo_tac. set n := (cpred _); move => [nN l1 l2]. case: (qleT_el yq (proj32_1 (finc _ nN))) => l3 //. move:( simple_interpolation2_pa nN (finc _ nN)). set A := simple_interpolation2 _ _ _; move => [qa qb qc qd]. case: (equal_or_not y (f n)) => eq1. by rewrite eq1 - (Hj _ nN); exists (yk n) => //; apply/ qlt0xP/ykp0. rewrite qa qb in qd;move: (qd _ (conj l1 (conj l3 eq1))) => [z [ za zb ->]]. move: (ykp5 _ _ nN (conj za (proj1 zb))) => [ua ub uc]. by move:(Hi _ ua ub); rewrite - uc -/A => <-; exists z => //; apply / qlt0xP. have fs: forall i j, i <c j -> natp j -> f j <q f i. move => i j h1 h2; rewrite - (cdiff_pr (proj1 h1)). move: (cpred_pr (NS_diff i h2) (cdiff_nz h1)) => [sa ->]. move:(NS_lt_nat h1 h2) => iN; move: (cpred (j -c i)) sa; clear h1 h2. apply:Nat_induction;first by rewrite (csum_nS _ NS0) (Nsum0r iN); apply:finc. move => n nN Hrec; apply:(qlt_ltT _ Hrec). by rewrite(csum_nS _ (NS_succ nN)); apply: (finc _ (NS_sum iN (NS_succ nN))). have fs': forall i j, i <=c j -> natp j -> f j <=q f i. move => i j lt1 nj; case: (equal_or_not i j) => eq. rewrite eq; apply: (qleR (Ha _ nj)). exact: (proj1 (fs _ _ (conj lt1 eq) nj)). have Hl: forall x, \0q <q x -> x <=q \1q -> g x <=q f \0c. move=> x ha hb; move:(proj2 (Hk _ ha hb)) => le1. move:(xnp1 _ (proj32_1 ha)) => iN. exact: (qleT le1 (fs' _ _ (cle0n iN) iN)). have rc: forall x y, inc x BQps -> inc y BQps -> x <q y -> g x <q g y. move => x y xp yp lxy;move: (lxy) => [[xq yq _] _]. move/ qlt0xP: (xp) => xp1; move/ qlt0xP: (yp) => yp1. case:(qleT_el xq QS1);case:(qleT_el yq QS1) => h1 h2. + have ilxy: BQinv y <q BQinv x by apply/BQinv_mon2. move:(xnp1 _ xq) (xnp1 _ yq) => ixN iyN. move:(BQfloor_M (proj1 ilxy)); rewrite (xnp2 _ yp1 h1) (xnp2 _ xp1 h2). move/(zle_cN (NS_succ iyN) (NS_succ ixN)). move /(cleSSP (CS_nat iyN) (CS_nat ixN)) => lixy. case: (equal_or_not (xn y) (xn x)) => eq1. rewrite(Hi _ xp1 h2) (Hi _ yp1 h1) eq1. move:(simple_interpolation2_pa ixN (finc _ ixN)) => [_ _ sa _]. by apply: sa. move: (proj2 (Hk _ xp1 h2)) (proj1 (Hk _ yp1 h1)) => sa sb. move/(cleSltP iyN): (conj lixy eq1) => sc. exact:(qle_ltT (qleT sa (fs' _ _ sc ixN)) sb). + exact:(qle_ltT (Hl _ xp1 h2) (Hc _ h1)). + by case: (proj2 (qlt_ltT lxy (qle_ltT h1 h2))). + move:(Ha _ NS0) (QSo QS1) => ha hb. rewrite (Hb _ h1) (Hb _ h2) /BQdiff - (BQsumA xq ha hb) - (BQsumA yq ha hb). by apply/(BQsum_lt2r xq yq (QSs ha hb)). have bg: bijection (Lf g BQps Z). apply: lf_bijective => // u v up vp sg. case:(qleT_ell (BQps_sBQ up) (BQps_sBQ vp)) => // h. by move: (proj2 (rc _ _ up vp h)). by move: (nesym (proj2 (rc _ _ vp up h))). move:BQor_or BQor_sr => or sr. move:(BQps_sBQ); rewrite - sr => sa. have to1:= (total_order_sub BQor_tor sa). move: (iorder_osr or sa) => [or1 sr1] {sa}. have: sub Z BQ by apply:Zo_S. rewrite - sr => sa;move: (iorder_osr or sa) => [or2 sr2] {sa}. apply:total_order_isomorphism => //; [by rewrite sr1; aw | by rewrite sr2; aw | ]. aw; move => x y xp yp /=; rewrite !LfV// => /iorder_gle1 /BQle_P lxy. apply/iorder_gle0P; [by apply: ra | by apply: ra | apply/BQle_P]. case: (equal_or_not x y) => eq1. rewrite eq1; exact: (qleR (Zo_S (ra _ yp))). exact: (proj1 (rc _ _ xp yp (conj lxy eq1))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)