If not equal implies apart, Markov's principle follows

[jkingdon]

The proof is similar to https://us.metamath.org/ileuni/trilpo.html and https://us.metamath.org/ileuni/redcwlpo.html and uses some of the same lemmas.