generalization of lime_sup lemmas to limf_sup

[affeldt-aist]

analysis/theories/realfun.v

Line 611 in 8196991

Lemma lime_sup_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_sup f a.

"Most of the important lemmas like this one are probably true of limf_sup. At least lime_sup_ge0,, lime_supD, lime_inf_sup, and lim_lime_inf. There may be some conditions to replace with \forall x \near F, but otherwise I'm hoping it just works." @zstone1