---

Step * 1 1 of Lemma req-rat2real


1. q1 : ℚ
2. q2 : ℚ
3. rat2real(q1) = rat2real(q2)
4. rat2real(q1) ≠ rat2real(q2)
⊢ q1 = q2 ∈ ℚ
BY
{ ((Assert ⌜False⌝⋅ THEN Auto) THEN RWO "-2" (-1) THEN Auto THEN MoveToConcl (-1) THEN Fold `not` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  q1  :  \mBbbQ{}
2.  q2  :  \mBbbQ{}
3.  rat2real(q1)  =  rat2real(q2)
4.  rat2real(q1)  \mneq{}  rat2real(q2)
\mvdash{}  q1  =  q2


By

---

Latex:
((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  RWO  "-2"  (-1)
  THEN  Auto
  THEN  MoveToConcl  (-1)
  THEN  Fold  `not`  0
  THEN  Auto)

---

Home Index