`Lnorm0`

[affeldt-aist]

https://github.com/math-comp/analysis/blob/c5ea0abfda9c1ec4f223ea2e013de20fbf23135f/theories/hoelder.v#L86

Try to change this lemma to have no condition when enabling (mu (f @^-1` (setT `\ 0%R))) when p = 0 (which looks like a saner convention than the current one).

@CohenCyril @proux01 @hoheinzollern @t6s