proposition: Lemma limitR_unique x v1 v2: BR_seq x -> realp v1 -> realp v2 -> limitR x v1 -> limitR x v2 -> v1 = v2.
proof: Proof. move => pa v1q v2q ha hb. ex_middle ne. have dq:= (RS_diff v2q v1q). set d := BRhalf (BRabs (v2 -r v1)). have dp: inc d BRps. by apply:BRhalf_pos; apply:RpsSa => // /(BRdiff_xx_rw v2q v1q) eq1; case:ne. move/limitR_alt: ha => ha1. move/limitR_alt: hb => hb1. move: (ha1 _ dp) (hb1 _ 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: realp (Vg x m) by apply: (BR_seq_prop pa mN). move: (rle_triangular (RS_diff he v1q) (RS_diff v2q he)). rewrite - (BRdiff_sum_comm he (RS_diff v2q he) v1q) (BRsum_diff he v2q). move:(BRsum_Mltlt hc hd);rewrite (BRdouble_half1 (RSa dq)). rewrite (BRabs_diff v2q he) => sa sb; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)