proposition: Lemma interpolation_prop1 n u v (f := simple_interpolation n u v): inc n BQ -> u <q v -> [/\ f n = u, f (n +q \1q) = v, (forall x, n <=q x -> x <=q (n +q \1q) -> (u <=q f x /\ f x <=q v)), (forall y, u <=q y -> y <=q v -> exists x, [/\ n <=q x, x <=q (n +q \1q) & y = f x]) & (forall x y, x <q y -> f x <q f y)].
proof: Proof. move => nq lt1. move:(lt1) => [[uq vq le1] ne1]. have qa: inc (v -q u) BQps by apply/ qlt0xP; apply/ (qlt_diffP1 uq vq). move/BQps_iP: (qa) => [qb nuv]. move:(BQp_sBQ qb) => qc. split. + rewrite /f /simple_interpolation (BQdiff_xx nq). by rewrite (BQprod_0r qc) (BQsum_0l). + rewrite /f /simple_interpolation (BQdiff_sum nq QS1). by rewrite (BQprod_1r qc) BQsumC BQsum_diff. + move => x sa sb. rewrite /f /simple_interpolation. set y := (v -q u) *q (x -q n). have yp: inc y BQp. by apply: QpS_prod => //; apply/ (qle_diffP nq (proj32 sa)). split; first by rewrite BQsumC; apply:BQsum_Mp. move/(BQsum_le2r (proj31 sb) (proj32 sb) (QSo nq)): sb. rewrite -/(_ -q _) -/(_ -q _) (BQdiff_sum nq QS1) => ha. move/(BQprod_ple2r (proj31 ha) QS1 qa): ha. rewrite BQprodC -/y (BQprod_1l qc) => hb. move/(BQsum_le2r (proj31 hb) (proj32 hb) uq): hb. by rewrite (BQsumC (v -q u)) BQsum_diff. + move => y uy yv. move:(proj32 uy) => yq. rewrite /f /simple_interpolation. move /(BQsum_le2r uq yq (QSo uq)): uy. rewrite -/(_ -q _) -/(_ -q _) (BQdiff_xx uq) => l2. move /(BQsum_le2r yq vq (QSo uq)): yv; rewrite -/(_ -q _) -/(_ -q _) => l3. move:(QpsS_inv qa) => /BQps_sBQp => l4. move: (BQprod_Mlege0 l4 l2) (BQprod_Mlege0 l4 l3). rewrite (BQprod_0l (BQp_sBQ l4)) BQprod_inv1 // -/(_ /q _). set z := (y -q u) /q (v -q u); move => l5 l6. move:(proj31 l6) => zq. move /(BQsum_le2r (proj31 l6) (proj32 l6) nq): l6. move /(BQsum_le2r QS0 (proj32 l5) nq): l5. rewrite (BQsum_0l nq)(BQsumC \1q n) => l7 l8. exists (z +q n); split => //. have qd:= (proj32 l2). have qe: inc (BQinv (v -q u)) BQ by apply:QS_inv. rewrite (BQsumC z) (BQdiff_sum nq zq) /z BQprodA // -/(_ /q _). rewrite (BQdiv_prod qc qd nuv) BQsumC (BQsum_diff) //. + move => x y lxy; rewrite /f /simple_interpolation. move: (lxy) => [[xq yq _] _]. move/ (BQsum_lt2r xq yq (QSo nq)): lxy => ha. move: (BQprod_Mltgt0 qa ha); rewrite (BQprodC) (BQprodC _ (v -q u) ) => hd. by move/(BQsum_lt2r (proj31_1 hd) (proj32_1 hd) uq): hd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)