outdated comment?

[affeldt-aist]

analysis/theories/normedtype.v

Lines 2666 to 2724 in f6ada5b

	(* TODO: Remove R_complete_lim and use lim instead *)
	(* Definition R_lim (F : (R -> Prop) -> Prop) : R := *)
	(* sup (fun x : R => `[<F (ball (x + 1) 1)>]). *)
	(* move: (Lub_Rbar_correct (fun x : R => F (ball (x + 1) 1))). *)
	(* move Hl : (Lub_Rbar _) => l{Hl}; move: l => [x| |] [Hx1 Hx2]. *)
	(* - case: (HF (Num.min 2 eps%:num / 2)%:pos) => z Hz. *)
	(* have H1 : z - Num.min 2 eps%:num / 2 + 1 <= x + 1. *)
	(* rewrite ler_add //; apply/RleP/Hx1. *)
	(* apply: filterS Hz. *)
	(* rewrite /ball /= => u; rewrite /AbsRing_ball absrB ltr_distl. *)
	(* rewrite absrB ltr_distl. *)
	(* case/andP => {Hx1 Hx2 FF HF x F} Bu1 Bu2. *)
	(* have H : Num.min 2 eps%:num <= 2 by rewrite ler_minl lerr. *)
	(* rewrite addrK -addrA Bu1 /= (ltr_le_trans Bu2) //. *)
	(* rewrite -addrA ler_add // -addrA addrC ler_subr_addl. *)
	(* by rewrite ler_add // ler_pdivr_mulr // ?mul1r. *)
	(* have H2 : x + 1 <= z + Num.min 2 eps%:num / 2 + 1. *)
	(* rewrite ler_add //; apply/RleP/(Hx2 (Finite _)) => v Hv. *)
	(* apply: Rbar_not_lt_le => /RltP Hlt. *)
	(* apply: filter_not_empty. *)
	(* apply: filterS (filterI Hz Hv). *)
	(* rewrite /ball /= => w []; rewrite /AbsRing_ball //. *)
	(* rewrite absrB ltr_distl => /andP[_ Hw1]. *)
	(* rewrite absrB ltr_distl addrK => /andP[Hw2 _]. *)
	(* by move: (ltr_trans (ltr_trans Hw1 Hlt) Hw2); rewrite ltrr. *)
	(* apply: filterS Hz. *)
	(* rewrite /ball /= => u; rewrite /AbsRing_ball absrB absRE 2!ltr_distl. *)
	(* case/andP => {Hx1 Hx2 F FF HF} H H0. *)
	(* have H3 : Num.min 2 eps%:num <= eps by rewrite ler_minl lerr orbT. *)
	(* apply/andP; split. *)
	(* - move: H1; rewrite -ler_subr_addr addrK ler_subl_addr => H1. *)
	(* rewrite ltr_subl_addr // (ltr_le_trans H0) //. *)
	(* rewrite -ler_subr_addr (ler_trans H1) //. *)
	(* rewrite -ler_subr_addl -!addrA (addrC x) !addrA subrK. *)
	(* rewrite ler_subr_addr -mulrDl ler_pdivr_mulr //. *)
	(* by rewrite -mulr2n -mulr_natl mulrC ler_pmul. *)
	(* - move: H2; rewrite -ler_subr_addr addrK. *)
	(* move/ler_lt_trans; apply. *)
	(* move: H; rewrite // ltr_subl_addr => H. *)
	(* rewrite -ltr_subr_addr (ltr_le_trans H) //. *)
	(* rewrite addrC -ler_subr_addr -!addrA (addrC u) !addrA subrK. *)
	(* rewrite -ler_subl_addr opprK -mulrDl ler_pdivr_mulr // -mulr2n -mulr_natl. *)
	(* by rewrite mulrC ler_pmul. *)
	(* - case (HF 1%:pos) => y Fy. *)
	(* case: (Hx2 (y + 1)) => x Fx. *)
	(* apply: Rbar_not_lt_le => Hlt. *)
	(* apply: filter_not_empty. *)
	(* apply: filterS (filterI Fy Fx) => z [Hz1 Hz2]. *)
	(* apply: Rbar_le_not_lt Hlt; apply/RleP. *)
	(* rewrite -(ler_add2r (-(y - 1))) opprB !addrA -![in X in _ <= X]addrA. *)
	(* rewrite (addrC y) ![in X in _ <= X]addrA subrK. *)
	(* suff : `|x + 1 - y|%R <= 1 + 1 by rewrite ler_norml => /andP[]. *)
	(* rewrite ltrW // (@subr_trans _ z). *)
	(* by rewrite (ler_lt_trans (ler_norm_add _ _)) // ltr_add // distrC. *)
	(* - case: (HF 1%:pos) => y Fy. *)
	(* case: (Hx1 (y - 1)); by rewrite addrAC addrK. *)
	(* Qed. *)
	(* Admitted. *)