proposition: Lemma limitR_same x y z: BR_seq x -> BR_seq y -> realp z -> similar_seq x y -> limitR x z -> limitR y z.
proof: Proof. move=> sx sy zr H l1 e ep. move: (BQhalf_pos ep)(QS_half (BQps_sBQ ep)) => hep hq. move: (H _ hep) (l1 _ hep) => [n na nb] [m ma mb]. move:(cmax_p1 (CS_nat na)(CS_nat ma)); set k := cmax n m; move => [ka kb]. have kN: natp k by apply:Gmax_E. exists k => // q qn kq. move:(nb _ qn (cleT ka kq))(mb _ qn (cleT kb kq)) => hc hd. have: realp (Vg x q) by apply:BR_seq_prop. have: realp (Vg y q) by apply: BR_seq_prop. move => ha hb; move:(rle_triangular (RS_diff ha hb) (RS_diff hb zr)). rewrite (BRsumA (RS_diff ha hb) hb (RSo zr))(BRsum_diff1 hb ha). move: (BRsum_Mltlt hc hd); rewrite (BRabs_diff hb ha). rewrite (BRsum_cQ hq hq) (BQdouble_half1 (BQps_sBQ ep)) => sa sb. BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)