Yes, it may be possible to convert to a common type - but that will involve extra work at runtime. If you need to prove the correctness of something and this makes that difficult for you, you're welcome to use a subset of the functionality.
Shouldn't the algorithm be provably correct on its own right? I hope that we're not building libraries where our strongest guarantee of correctness is, "It looks like it does the right thing".
Consider the case where the types differ only in some attribute like their allocator that doesn't change the behaviour of comparisons.
There is a way to define the algorithm over different types and still preserve the semantics of the ordering, and to do so without requiring conversions. I suspect that the case where types differ by an Allocator will satisfy those requirements.