`inf_lb` should be `inf_lbound`?

[IshiguroYoshihiro]

Should inf_lb be inf_lbound?
When I want to prove a goal that S x -> inf S <= x, I couldn't find inf_lb by searching with (inf _ <= _) or inf "le".

analysis/theories/reals.v

Line 398 in 59fb6d2

Lemma inf_lb E : has_lbound E -> lbound E (inf E).

analysis/classical/classical_sets.v

Line 2908 in 59fb6d2

Definition lbound A : set T := [set y | forall x, A x -> (y <= x)%O].

[affeldt-aist]

I agree with the proposed renaming.

[affeldt-aist]

The search problem looks to me like a limitation of the Search that does not do any unfolding. Maybe there is a plan to address that. @proux01 ? @CohenCyril ?

[proux01]

Well, plans, there definitely are, for years. About effective actions, nothing on my side.