---

Step * 1 1 of Lemma assert-rat-term-eq2


1. r1 : rat_term()
2. r2 : rat_term()
3. f : ℤ ⟶ ℝ
4. tt ≤ rat-term-eq(r1;r2)
5. fst(rat_term_to_real(f;r2))
6. fst(rat_term_to_real(f;r1))
⊢ ↑rat-term-eq(r1;r2)
BY
{ InstLemma `bool-mono` [] }

1
1. r1 : rat_term()
2. r2 : rat_term()
3. f : ℤ ⟶ ℝ
4. tt ≤ rat-term-eq(r1;r2)
5. fst(rat_term_to_real(f;r2))
6. fst(rat_term_to_real(f;r1))
7. mono(𝔹)
⊢ ↑rat-term-eq(r1;r2)

---

Latex:

---

Latex:

1.  r1  :  rat\_term()
2.  r2  :  rat\_term()
3.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
4.  tt  \mleq{}  rat-term-eq(r1;r2)
5.  fst(rat\_term\_to\_real(f;r2))
6.  fst(rat\_term\_to\_real(f;r1))
\mvdash{}  \muparrow{}rat-term-eq(r1;r2)


By

---

Latex:
InstLemma  `bool-mono`  []

---

Home Index