proposition: Lemma CauchyQ_when_limit x: BQ_seq x -> (exists2 y, ratp y & limitQ x y) -> CauchyQ x.
proof: Proof. move => ha [y yq hb]; split => // e ep. move:(BQhalf_pos ep) => hep. move:(hb _ hep) => [N NN etc]; exists N => // n m nN mN na nb. move: (etc n nN na)(etc m mN nb) => sa sb. move:(BQsum_Mltlt sa sb); rewrite (BQdouble_half1 (BQps_sBQ ep))=> sc. have xnq: ratp (Vg x n) by apply: BQ_seq_prop. have xmq: ratp (Vg x m) by apply: BQ_seq_prop. move: (qle_triangular (QS_diff xnq yq) (QS_diff yq xmq)). rewrite (BQsumA (QS_diff xnq yq) yq (QSo xmq)) (BQsum_diff1 yq xnq). rewrite (BQabs_diff yq xmq) => sd; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)