On Wed, 2013-09-25 at 17:04 +0400, Sergei Meshveliani wrote: > Please, how to prove x < y → x ≤ y > > in the general setting under lib-0.7 ? > [..] Probably, it is by DecTotalOrder + Relation.Binary.StrictToNonStrict, that is the definition for _≤_ to be taken from StrictToNonStrict. I'll try and see. ------ Sergei