the proof of cvg_at_rightP should be shorter

[affeldt-aist]

analysis/theories/realfun.v

Line 111 in 8196991

Lemma cvg_at_rightP (f : R -> R) (p l : R) :

"In a textbook all four of these proofs would be three liners:

1. In first countable spaces, filter convergence <-> sequence convergence
2. The lower (upper) limit topology (AKA sogenfrey line) is first countable
3. All sequences in the lower (upper) limit topology that converge, do so from the left (right).

The proof you have is fine, I'm not complaining about it. I am complaining that some missing classical machinery is making these proofs longer than necessary." @zstone1