proposition: Lemma BRi_lowbound x d: realp x -> inc d BQps -> exists2 y, inc y x & forall z, inc z x -> y -q d <q z.
proof: Proof. move => xr dps; move: (BQps_sBQ dps) => dq. move/BR_P:(xr) => [pa pb pc pd pe]. move:(pb) (setC_ne (conj pa pc)) => [a ax] [b /setC_P [bq bnx]]. have aq:=(pa _ ax). case:(qleT_ell aq bq) => lab; first by case:bnx; rewrite - lab. by case:bnx; apply: (pd _ _ ax). move/(qlt_diffP1 bq aq): lab => / qlt0xP dp. have qq:=(QpsS_div dp dps). have [n nN lt1]:=(BQ_floorp4 ((BQps_sBQ qq))). pose prop m := ~inc (a -q (BQ_of_nat m) *q d) x. have prop3: prop n. move /(BQprod_plt2r (proj31_1 lt1) (proj32_1 lt1) dps): lt1. rewrite BQprodC (BQprod_div dq (BQps_sBQ dp) (BQps_nz dps)) => h1. move/(BQdiff_lt1P aq bq (proj32_1 h1)): h1 => h2. by move => h; case: bnx; apply:(pd _ _ h). case:(least_int_prop2 nN prop3). by rewrite /prop (BQprod_0l dq)(BQdiff_0r aq);move => []. set m := cpred _;move => [mN ma /excluded_middle]; set c:= (a -q _) => cx. have ncx: ~ (inc (c -q d) x). move:(BZ_of_nat_i mN) => sa; move:(BQ_of_Z_iQ sa) => sb. have pq:=(QSp sb dq). move: ma; rewrite /prop (Nsucc_rw mN) /BQ_of_nat - (BZsum_cN mN NS1). rewrite - (BQsum_cZ sa ZS1) (BQprodDl dq sb QS1) (BQprod_1l dq). by rewrite BQdiff_diff2. ex_tac. move => z zx. have cq:=(pa _ cx); have ddq:=(QS_diff cq dq). case: (qleT_ell ddq (pa _ zx)). + by move => eq; case: ncx; rewrite eq. + exact. + move => leq; case: ncx; apply:(pd _ _ zx leq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)