proposition: Lemma limitQ_unique x v1 v2: BQ_seq x -> ratp v1 -> ratp v2 -> limitQ x v1 -> limitQ x v2 -> v1 = v2.
proof: Proof. move => pa v1q v2q ha hb. ex_middle ne. have dq:= (QS_diff v2q v1q). set d := BQhalf(BQabs (v2 -q v1)). have dp: inc d BQps. apply:BQhalf_pos; apply/BQps_iP; split; first by apply:QpSa. by apply /(BQabs0_bis dq) =>/(BQdiff_xx_rw v2q v1q) eq1; case:ne. move: (ha _ dp) (hb _ dp)=> [n1 n1N na][n2 n2N nb]. move:(cmax_p1 (CS_nat n1N)(CS_nat n2N)); set m := cmax n1 n2; move => [ma mb]. have mN: natp m by apply:Gmax_E. move:(na _ mN ma)(nb _ mN mb) => hc hd. have he: inc (Vg x m) BQ by apply: (BQ_seq_prop pa mN). move: (qle_triangular (QS_diff he v1q) (QS_diff v2q he)). rewrite - (BQdiff_sum_comm he (QS_diff v2q he) v1q) (BQsum_diff he v2q). move:(BQsum_Mltlt hc hd);rewrite (BQdouble_half1 (QSa dq)). rewrite (BQabs_diff v2q he) => sa sb; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)