Bounded and landau notations

[mkerjean]

After PR#267 is merged, should we add to landau.v lemmas about bounded functions using landau notations ? This is needed for Banach-Steinhauss for example.

NB(rei): PR #267 has been closed but its contents made their was through another PR

[affeldt-aist]

Update: Note that PR #267 has been closed and split into PR #283 (now merged) and PR #183 (to be merged shortly)