proposition: Lemma multiple_interpolation_prop f (g := multiple_interpolation (fun z => (BQ_of_nat (f z)))): (forall n, natp n -> natp (f n)) -> (forall n, natp n -> f n <c f(csucc n)) -> (f \0c) = \0c -> [/\ forall x, inc x BQp -> inc (g x) BQp, (forall y, inc y BQp -> exists2 x, inc x BQp & g x = y), (forall n, natp n -> g (BQ_of_nat n) = BQ_of_nat (f n)) & forall x y, inc x BQp -> x <q y -> g x <q g y].
proof: Proof. move => h1 h2 h3. pose F n := (BQ_of_nat (f n)). have pa: forall n, natp n -> forall x, (BQ_of_nat n) <=q x -> x <q ((BQ_of_nat n) +q \1q) -> g x = simple_interpolation (BQ_of_nat n) (F n) (F (csucc n)) x. move => n nN x pa pb. move:(proj32 pa) => xq. move: (BQ_floorp2 xq (BZ_of_nat_i nN) (conj pa pb)) => e1. by rewrite /g /multiple_interpolation - e1 BZ_of_nat_val. have pc: forall x, inc x BQp -> let m := (BQfloor x) in g x = simple_interpolation (BQ_of_nat (P m)) (F (P m)) (F (csucc (P m))) x. move => x xp m. move: (BQfloor_pos xp) => [sa sb]. move: (BQ_floorp (BQp_sBQ xp)); rewrite sa; move => [ma mb]. exact:(pa _ sb _ ma mb). have pd: forall n, natp n -> F n <q F (csucc n). by move => n nN; move/(qlt_cN (h1 _ nN) (h1 _ (NS_succ nN))): (h2 _ nN). have rc:forall n, natp n -> g (BQ_of_nat n) = F n. move => n nN; move:(QpS_of_nat nN) => xp; move: (BQp_sBQ xp) => xq. have sb: P (BQfloor (BQ_of_nat n)) = n. by rewrite /BQ_of_nat (BQfloor_Z (BZ_of_nat_i nN))/BZ_of_nat; aw. move:(pc _ xp) => /=; rewrite sb; rewrite /simple_interpolation. have sc: ratp (F n) by apply:QS_of_nat; apply: h1. have sd: ratp (F (csucc n)) by apply:QS_of_nat; apply: h1; fprops. by rewrite (BQdiff_xx xq) (BQprod_0r (QS_diff sd sc)) (BQsum_0l). have pf: forall x, let m := BQfloor x in inc x BQp -> F (P m) <=q g x /\ g x <q F (csucc (P m)). move => x m xp. move:(BQfloor_pos xp) (pc _ xp)=> [sa sb] gv. move:(pd _ sb) (BQfloor_pos2 xp) => sd [se sf]. move: (interpolation_prop2 (QS_of_nat sb) sd) => [ hc _ ]. by move: (hc _ se sf); rewrite - gv. have ra: forall x, inc x BQp -> inc (g x) BQp. move => x xq; move:(proj1 (pf _ xq)); move: (proj2 (BQfloor_pos xq)) => sa. have: inc (F (P (BQfloor x))) BQp by apply: QpS_of_nat;apply: h1. move / qle0xP => su sv; apply/ qle0xP; BQo_tac. have pg: forall k, natp k -> exists n, [/\ natp n, f n <=c k & k <c f (csucc n)]. apply: Nat_induction. exists \0c; move: (h2 _ NS0); rewrite h3 => sa; split => //; fprops. move => k kN [m [ma mb mc]]. move /(cleSltP kN): mc; case: (equal_or_not (csucc k) (f (csucc m))). move => eq1; exists (csucc m); rewrite eq1; split => //; fprops. by move => sa sb; exists m; split => //; move: (cleS kN) => /(cleT mb). have rb: forall y, inc y BQp -> exists2 x, inc x BQp & g x = y. move => y yq. move: (BQfloor_pos2 yq) (BQfloor_pos yq) => /=; set k:= (P (BQfloor y)). move => [sa sb] [sc sd]. move:(pg _ sd) => [m [mN ma mb]]. have mc: (F m) <=q BQ_of_nat k by apply/ qle_cN; fprops. have se: inc (BZ_of_nat k) BZp by apply:BZ_of_natp_i. have md: BQ_of_nat k +q \1q <=q BQ_of_nat (f (csucc m)). by rewrite (BQ_of_nat_succ sd); apply/ qle_cN; fprops; apply/cleSltP. move:(qleT mc sa) (qlt_leT sb md) =>la lb. move: (pd _ mN) (QS_of_nat mN) => ub ua. move: (proj2 (interpolation_prop2 ua ub) _ la lb) => [x [xa xb yv]]. have / qle0xP cp: inc (BQ_of_nat m) BQp by apply:QpS_of_nat. have xp: inc x BQp by apply/ qle0xP; BQo_tac. have sse: inc (BZ_of_nat m) BZ by apply:BZ_of_nat_i. move: (BQ_floorp2 (BQp_sBQ xp) sse (conj xa xb)) => h. by ex_tac; rewrite (pc _ xp) yv - h /BZ_of_nat pr1_pair. split => //. move => x y xp lxy; move: (proj1 lxy) => lexy. have yp: inc y BQp by move/ qle0xP: xp => sa;apply/ qle0xP; BQo_tac. move: (BQfloor_M lexy) =>ha. move:(pc _ xp) (pc _ yp) (BQfloor_pos xp) => gx gy [sa sb]. move:(pd _ sb) (BQfloor_pos2 xp) => sd [se sf]. move: (interpolation_prop1 (QS_of_nat sb) sd) => [_ hc _ _ hd]. case: (equal_or_not (BQfloor x) (BQfloor y)) => sff. by move: (hd x y lxy); rewrite - gx sff - gy. move: (hd _ _ sf); rewrite hc - gx => eq1. move:(BQfloor_pos yp) => [sa' sb']. move:(pd _ sb') (BQfloor_pos2 yp) => sd' [se' sf']. move: (interpolation_prop1 (QS_of_nat sb') sd') => [hb' hc' _ _ hd']. have fmon: forall a b, natp a -> natp b -> a <c b -> f (csucc a) <=c f b. move => a b aN bN lab. move /(cleSltP aN): lab => h; rewrite -(cdiff_pr h). move:(NS_diff (csucc a) bN); move:(b -c csucc a); apply: Nat_induction. rewrite (csum0r (CS_succ a)); fprops. move => n nN Hrec; apply (cleT Hrec). rewrite (csum_nS _ nN); exact (proj1(h2 _ (NS_sum (NS_succ aN) nN))). have la: F (csucc (P (BQfloor x))) <=q F (P (BQfloor y)). have h: BQfloor x <z BQfloor y by split. have qqa: natp (P (BQfloor x)) by []. have qqb: natp (P (BQfloor y)) by []. move / (qlt_cZ (proj31_1 h) (proj32_1 h)) : h. rewrite sa sa' => /(qlt_cN qqa qqb) qge0x. apply/ qle_cN; [by apply: h1; fprops | by apply: h1 | by apply: fmon]. move:(qlt_leT eq1 la) => lb. case: (equal_or_not (BQ_of_nat (P (BQfloor y))) y) => hh. by rewrite gy - {4} hh hb'. move:(hd' _ _ (conj se' hh)); rewrite hb' - gy => lc; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)