---

Step * 1 of Lemma div_unique2


1. a : ℕ
2. n : ℕ+
3. p : ℕ
4. Div(a;n;p)
5. q : ℕ
6. Div(a;n;q)
7. (a ÷ n) = q ∈ ℤ
⊢ (a ÷ n) = p ∈ ℤ
BY
{ (FLemma `div_unique` [-4;-2] THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  p  :  \mBbbN{}
4.  Div(a;n;p)
5.  q  :  \mBbbN{}
6.  Div(a;n;q)
7.  (a  \mdiv{}  n)  =  q
\mvdash{}  (a  \mdiv{}  n)  =  p


By

---

Latex:
(FLemma  `div\_unique`  [-4;-2]  THEN  Auto)

---

Home Index