1. q1 : ℚ
2. q2 : ℚ
3. rat2real(q1) = rat2real(q2)
⊢ q1 = q2 ∈ ℚ
{ (SupposeNot THEN (RWO "rneq-rat2real<" (-1) THENA Auto)) }
4. rat2real(q1) ≠ rat2real(q2)