Rework landau's documentation and naming convention

[drouhling]

This is related to #101. [NB(rei): PR which has been merged]

[NB(rei): partially addressed by PR #216 ]

Since we force user to use the equational notations by removing the defintions, we should be very clear on how to use this library. In particular the documentation should:

• detail how to state a lemma using the notations, e.g. should I use f =O_F g or f = [O_F g of h]?

• list all the possibilities to prove such relations, with the important steps, e.g. apply: eqoE is not to be forgotten, filter reasoning is possible but thought of as a last resort…

• clarify anything that can confuse the user about the notations, e.g.:

  • what is the difference between f =o_F g and f = o_F g?
  • why does f =O_ (0 : U) g work but not f =O_(0 : U) g, while f =O_F g does work?

• what are the naming conventions. I believe this library should be used as bigop: since it is hard and tedious to search lemmas using notations, we should have a clear naming convention so that it is easy to find a lemma by its name.

[affeldt-aist]

• detail how to state a lemma using the notations, e.g. should I use f =O_F g or f = [O_F g of h]?

This one is (now?) explained in the header.

• list all the possibilities to prove such relations, with the important steps, e.g. apply: eqoE is
  not to be forgotten, filter reasoning is possible but thought of as a last resort…

This should maybe go to PR #197 .

• clarify anything that can confuse the user about the notations, e.g.:

  • why does f =O_ (0 : U) g work but not f =O_(0 : U) g, while f =O_F g does work?

So we should at least add somewhere that "=O_(" is only valid in the syntax "=O_(x \near F)",
not in the syntax "=O_(x : U)".

By the way, it seems that the syntax "=O_(x \near F)" is not documented in the header.

[CohenCyril]

So we should at least add somewhere that "=O_(" is only valid in the syntax "=O_(x \near F)",
not in the syntax "=O_(x : U)"

Yes indeed, this should be documented, but we should also find a way to fix the parser so that we do not have to document it in the end 😆