proposition: Lemma contraction_cvg : cvgn y.
proof: Proof. apply/cauchy_cvgP; apply/cauchy_ballP => _/posnumP[e]; near_simpl. have lt_min n m : `|y n - y m| <= C * q%:num ^+ minn n m. wlog : n m / (n <= m)%N => W. by case/orP: (leq_total n m) => /W //; rewrite distrC minnC. by rewrite (minn_idPl _)// (le_trans _ (contraction_dist _ (m - n)))// subnKC. case: ltrgt0P C_ge0 => // [Cpos|C0] _; last first. near=> n m => /=; rewrite -ball_normE. by apply: (le_lt_trans (lt_min _ _)); rewrite C0 mul0r. near=> n; rewrite -ball_normE /= (le_lt_trans (lt_min n.1 n.2)) //. rewrite // -ltr_pdivlMl //. suff : ball 0 (C^-1 * e%:num) (q%:num ^+ minn n.1 n.2). by rewrite /ball /= sub0r normrN ger0_norm. near: n; rewrite nbhs_simpl. pose g := fun w : nat * nat => q%:num ^+ minn w.1 w.2. have := @fcvg_ball _ _ (g @ filter_prod \oo \oo) _ 0 _ (C^-1 * e%:num). move: (@cvg_geometric _ 1 q%:num); rewrite ger0_norm // => /(_ q1) geo. near_simpl; apply; last by rewrite mulr_gt0 // invr_gt0. apply/cvg_ballP => _/posnumP[delta]; near_simpl. have [N _ Q] : \forall N \near \oo, ball 0 delta%:num (geometric 1 q%:num N). exact: (@fcvg_ball R R _ _ 0 geo). exists ([set n | N <= n], [set n | N <= n])%N; first by split; exists N. move=> [n m] [Nn Nm]; rewrite /ball /= sub0r normrN ger0_norm /g //. apply: le_lt_trans; last by apply: (Q N) => /=. rewrite sub0r normrN ger0_norm /geometric //= mul1r. by rewrite ler_wiXn2l // ?ltW // leq_min Nn. Unshelve. all: end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau