Remove outdated comment

[affeldt-aist]

analysis/theories/normedtype.v

Lines 436 to 503 in 3f7d5f0

	(*Global Instance ereal_locally'_filter :
	forall x : {ereal R}, ProperFilter (ereal_locally' x).
	Proof.
	case=> [x||]; first exact: Proper_locally'_numFieldType.
	- apply Build_ProperFilter.
	by move=> P [M [Mreal MP]]; exists (M + 1); apply MP; rewrite ltr_addl.
	split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]].
	+ by exists 0; rewrite real0.
	+ have [/eqP MP0|MP0] := boolP (MP == 0).
	have [/eqP MQ0|MQ0] := boolP (MQ == 0).
	by exists 0; rewrite real0; split => // x x0; split;
	[apply/gtMP; rewrite MP0 | apply/gtMQ; rewrite MQ0].
	exists `|MQ|; rewrite realE normr_ge0; split => // x Hx; split.
	by apply gtMP; rewrite (le_lt_trans _ Hx) // MP0.
	by apply gtMQ; rewrite (le_lt_trans _ Hx) // real_ler_normr // lexx.
	have [/eqP MQ0|MQ0] := boolP (MQ == 0).
	exists `|MP|; rewrite realE normr_ge0; split => // x MPx; split.
	by apply gtMP; rewrite (le_lt_trans _ MPx) // real_ler_normr // lexx.
	by apply gtMQ; rewrite (le_lt_trans _ MPx) // MQ0.
	have {}MP0 : 0 < `|MP| by rewrite normr_gt0.
	have {}MQ0 : 0 < `|MQ| by rewrite normr_gt0.
	exists (Num.max (PosNum MP0) (PosNum MQ0))%:num.
	rewrite realE /= posnum_ge0 /=; split => // x.
	rewrite pos_lt_maxl /= => /andP[MPx MQx]; split.
	by apply/gtMP; rewrite (le_lt_trans _ MPx) // real_ler_normr // lexx.
	by apply/gtMQ; rewrite (le_lt_trans _ MQx) // real_ler_normr // lexx.
	+ by exists M; split => // ? /gtM /sPQ.
	- apply Build_ProperFilter.
	+ move=> P [M [Mr ltMP]]; exists (M - 1).
	by apply: ltMP; rewrite gtr_addl oppr_lt0.
	+ split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]].
	* by exists 0; rewrite real0.
	* have [/eqP MP0|MP0] := boolP (MP == 0).
	have [/eqP MQ0|MQ0] := boolP (MQ == 0).
	by exists 0; rewrite real0; split => // x x0; split;
	[apply/ltMP; rewrite MP0 | apply/ltMQ; rewrite MQ0].
	exists (- `|MQ|); rewrite realN realE normr_ge0; split => // x xMQ; split.
	by apply ltMP; rewrite (lt_le_trans xMQ) // MP0 ler_oppl oppr0.
	apply ltMQ; rewrite (lt_le_trans xMQ) // ler_oppl -normrN.
	by rewrite real_ler_normr ?realN // lexx.
	* have [/eqP MQ0|MQ0] := boolP (MQ == 0).
	exists (- `|MP|); rewrite realN realE normr_ge0; split => // x MPx; split.
	apply ltMP; rewrite (lt_le_trans MPx) // ler_oppl -normrN.
	by rewrite real_ler_normr ?realN // lexx.
	by apply ltMQ; rewrite (lt_le_trans MPx) // MQ0 ler_oppl oppr0.
	have {}MP0 : 0 < `|MP| by rewrite normr_gt0.
	have {}MQ0 : 0 < `|MQ| by rewrite normr_gt0.
	exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num).
	rewrite realN realE /= posnum_ge0 /=; split => // x.
	rewrite ltr_oppr pos_lt_maxl => /andP[].
	rewrite ltr_oppr => MPx; rewrite ltr_oppr => MQx; split.
	apply/ltMP; rewrite (lt_le_trans MPx) //= ler_oppl -normrN.
	by rewrite real_ler_normr ?realN // lexx.
	apply/ltMQ; rewrite (lt_le_trans MQx) //= ler_oppl -normrN.
	by rewrite real_ler_normr ?realN // lexx.
	* by exists M; split => // x /ltM /sPQ.
	Qed.
	Typeclasses Opaque ereal_locally'.*)
	(*Global Instance ereal_locally_filter :
	forall x, ProperFilter (@ereal_locally R x).
	Proof.
	case=> [x||].
	exact: ereal_locally_filter.
	exact: (ereal_locally'_filter +oo).
	exact: (ereal_locally'_filter -oo).
	Qed.
	Typeclasses Opaque ereal_locally.*)

This is can be safely removed since these Instances are available as lemmas
ereal_dnbhs_filter and ereal_nbhs_filter in ereal.v.