proposition: Lemma limit_positive xn x: (forall n, natp n -> \0r <=r (Vg xn n)) -> BR_seq xn -> limitR xn x -> realp x -> \0r <=r x.
proof: Proof. move => pa pb pc xr; move/BR_i0P: (xr); case; last by move/ rle0xP. move/BRopp_negative1 => ha;move/BRcompare_zero: (ha) => [e ea eb]. move/ (rlt_diffP2 (proj31_1 eb) (proj32_1 eb)): (eb). rewrite /BRdiff; rewrite (BRopp_K xr) => / rgt0xP pec. move:(pc _ ea) => [n nN h]. move / rle0xP:(pa _ nN) => ed. have pd: inc (Vg xn n -r x) BRp by apply: (RpS_sum ed (BRps_sBRp ha)). move: (h _ nN (cleR (CS_nat nN))); rewrite (BRabs_pos pd) => ee. move/(BRsum_lt2r (proj31_1 ee) (proj32_1 ee) xr): ee. rewrite BRsumC (BRsum_diff xr (BRp_sBR ed)) => sa. move:(rlt_ltT sa pec) => / rgt0xP /BR_di_neg_pos //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)