To prove properties about a Haskell function in Coq, we have to translate the Haskell function to Coq. Proofs about Haskell func- tions are performed in various levels of detail. For example, some- times proofs are performed as if Haskell were a total language and sometimes we are interested in explicitly reasoning about effects like partiality, exceptions or tracing. By translating a Haskell func- tion into a Coq function that is parametrised over a monad, we can model all these cases. Moreover, we can reuse function definitions for different kinds of proofs by instantiating the monadic function with a concrete monad instance. In order to model Haskell correctly, all arguments of constructors have to be made monadic as well. Due to technical restrictions in Coq we cannot define data types that are lifted this way. In previous work we have shown that we can use free monads and container representations to model effect-generic programs. That is, we can define a single Coq function that can be used to model no effects as well as effects like partiality, exceptions, and tracing. As an additional benefit by proving a proposition for all containers we can reuse propositions when considering different kinds of effects. While in previous work we have only considered equational propositions, in this work we are considering inequational proposi- tions. More precisely, we consider proofs that relate two Haskell terms with respect to some partial order that models the intuition of being “less or equally defined”. As an example, we consider the default implementation of Peano multiplication and an improved implementation with respect to “strictness”. Our contributions are more examples of using our orig- inal framework and the application to inequational propositions.