proposition: Lemma simple_interpolation2_pa i u v (yk := fun k => (BQinv (BQ_of_nat (csucc k)))) (ya := yk i) (yb := yk (csucc i)) (f := simple_interpolation2 (csucc i) u v): natp i -> u <q v -> [/\ f yb = u, f ya = v,forall z1 z2, z1 <q z2 -> f z1 <q f z2 & forall a, (f yb) <q a /\ a <q (f ya) -> exists z, [/\ yb <q z, z <q ya & a = f z]].
proof: Proof. move => iN lt1; move: (lt1) => [[uq vq _] _]. move/(qlt_diffP2 uq vq):lt1 => uvn. move: (NS_succ iN) => siN; move: (NS_succ siN) => ssiN. move:(QS_diff uq vq) => uvq. have Ta :BQ_of_nat (csucc (csucc i)) <> \0q. move => /BQ_of_nat_injective; apply: succ_nz. have Tb :BQ_of_nat (csucc i) <> \0q. move => /BQ_of_nat_injective; apply: succ_nz. have Tc: ratp (BQ_of_nat (csucc i)) by apply:QS_of_nat. have Td: ratp (BQ_of_nat (csucc (csucc i))) by apply:QS_of_nat. have ra: f yb = u. rewrite /f/simple_interpolation2 /yb /yk. rewrite (BQprod_inv1 Td Ta) (BQdiff_xx QS1)(BQprod_0l (QS_of_nat siN)). rewrite (BQprod_0l uvq); apply: (BQdiff_0r uq). have rb: f ya = v. rewrite /f/simple_interpolation2 /ya /yk. rewrite {2} /BQdiff BQsumC (BQsum_div (QSo QS1) Td Tc Tb). rewrite - (BQ_of_nat_succ (NS_succ iN)) BQopp_1 (BQprod_m1l Tc). rewrite BQsumC -/(_ -q _) (BQdiff_sum Tc QS1) (BQdiv_1x Tc). rewrite (BQprodC (BQinv _)) (BQprod_inv1 Tc Tb) (BQprod_1l uvq). by rewrite (BQdiff_diff uq uq vq) (BQdiff_xx uq) (BQsum_0l vq). have rc: forall z1 z2, z1 <q z2 -> f z1 <q f z2. move => z1 z2 lt1; rewrite /f /simple_interpolation2. move: (lt1) => [[z1q z2q _] _]. move: (QS_diff (QSp Td z1q) QS1) (QS_diff (QSp Td z2q) QS1) => za zb. move: (QSp (QSp za Tc) uvq) (QSp (QSp zb Tc) uvq) => zc zd. apply /(BQsum_lt2l (QSo zc) (QSo zd) uq); apply :qlt_opp. apply: (BQprod_Mltlt0 uvn); apply:(BQprod_Mltgt0 (BQpsS_fromN iN)). apply/ (BQsum_lt2r (QSp Td z1q) (QSp Td z2q) (QSo QS1)). rewrite BQprodC (BQprodC _ z2); apply:(BQprod_Mltgt0 (BQpsS_fromN siN) lt1). have re: forall a, (f yb) <q a /\ a <q (f ya) -> exists z, [/\ yb <q z, z <q ya & a = f z]. move => a [ha hb]; move:(proj32_1 ha) => aq. move: ha hb; rewrite /f/simple_interpolation2. have sa1:= (QS_diff uq aq); have sa:= QSo sa1. have sb: inc (yk (csucc i)) BQ by apply: QS_inv. have sb': inc (yk i) BQ by apply: QS_inv. move: (QSp Td sb) (QSp Td sb') => sf sf'. move:(QS_diff sf QS1) (QS_diff sf' QS1) => sc sc'. move: (QSp sc Tc) (QSp sc' Tc) => sc1 sc1'. move: (QSp sc1 uvq) (QSp sc1' uvq) => sd sd'. move: (QS_div sa1 uvq) => se; move:(QS_div se Tc) => se'. have Te:= (BQpsS_fromN iN). have Tf:= (BQpsS_fromN siN). have eq1 : a = u -q (u -q a) by symmetry; apply: BQdiff_diff_simp. move: (BQprod_div uvq sa1 (BQms_nz uvn)); rewrite BQprodC => eq2. move:(BQprod_div Tc se Tb); rewrite BQprodC => eq3. rewrite eq1; move /(BQsum_lt2l (QSo sd) sa uq) => /(qlt_oppP sa1 sd) => lt1. move /(BQsum_lt2l sa (QSo sd') uq) => /(qlt_oppP sd' sa1); move: lt1. rewrite - eq2 - eq3; rewrite - eq3 in se. move/(BQprod_mlt2r sc1 se uvn) => lt1 /(BQprod_mlt2r se sc1' uvn); move: lt1. move/(BQprod_plt2r sc se' Te) => lt1 /(BQprod_plt2r se' sc' Te); move: lt1. move /(qlt_diffP4 se' sf QS1) => lt1 /(qlt_diffP3 se' sf' QS1); move: lt1. rewrite - {3} (BQdiff_sum1 QS1 se') -(BQprod_div Td (QSs se' QS1) Ta). rewrite ! (BQprodC (BQ_of_nat (csucc (csucc i)))). move/(BQprod_plt2r sb (QS_div (QSs se' QS1) Td) Tf) => lt1. move/(BQprod_plt2r (QS_div (QSs se' QS1) Td) sb' Tf). set x3 := _ /q _; move => lt3; exists x3; rewrite (BQprodC x3); done. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)