Florian, > facilitated by theorems "strict_mono_eq", "strict_mono_eq" and "strict_mono_eq". What is the difference between these? :) Amine.