---

Step * 1 of Lemma qdiv-one


1. q : ℚ
⊢ (q/1) = q ∈ ℚ
BY
{ xxx(InstLemma `qmul-qdiv-cancel` [⌜1⌝;⌜q⌝]⋅ THENA Auto)xxx }

1
1. q : ℚ
2. (1 * (q/1)) = q ∈ ℚ
⊢ (q/1) = q ∈ ℚ

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}
\mvdash{}  (q/1)  =  q


By

---

Latex:
xxx(InstLemma  `qmul-qdiv-cancel`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)xxx

---

Home Index