did anyone manage to cross the chasm between floats and reals doing proofs about algorithms in actual code? It might be a skill issue but I'm always stuck at reals not being decidably comparable