---

Step * 2 2 of Lemma proper-divisor_wf


1. n : ℕ+
2. y : Top
3. n < 5
4. ¬(n = 4 ∈ ℤ)
⊢ inr (λx.any x)  ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
BY
{ (RepUR ``decidable or sq_exists not`` 0 THEN Auto)⋅ }

1
1. n : ℕ+
2. y : Top
3. n < 5
4. ¬(n = 4 ∈ ℤ)
5. ∀n1:ℤ. (n1 < n ∧ (2 ≤ n1) ∧ (n1 | n) ∈ Type)
6. x : ℤ
7. x < n
8. 2 ≤ x
9. x | n
⊢ any x ∈ False

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  y  :  Top
3.  n  <  5
4.  \mneg{}(n  =  4)
\mvdash{}  inr  (\mlambda{}x.any  x)    \mmember{}  Dec(\mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))])


By

---

Latex:
(RepUR  ``decidable  or  sq\_exists  not``  0  THEN  Auto)\mcdot{}

---

Home Index