---

Step * 1 2 2 2 1 1 of Lemma decidable__proper_divisor


1. n : ℤ
2. n < 5
3. 2 ≤ n
4. n | 5
⊢ False
BY
{ ((CaseNat 2 `n'
    THEN Auto'
    THEN Try ((ElimVar `n' THEN (RWO "divides_iff_rem_zero" (-1)  THENM Reduce (-1)) THEN Auto)))⋅
   THEN ((CaseNat 3 `n'
          THEN Auto'
          THEN Try ((ElimVar `n' THEN (RWO "divides_iff_rem_zero" (-2)  THENM Reduce (-2)) THEN Auto)))
         THEN CaseNat 4 `n'
         THEN Auto'
         THEN Try ((ElimVar `n' THEN (RWO "divides_iff_rem_zero" (-3)  THENM Reduce (-3)) THEN Auto)))⋅
   ) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  n  <  5
3.  2  \mleq{}  n
4.  n  |  5
\mvdash{}  False


By

---

Latex:
((CaseNat  2  `n'
    THEN  Auto'
    THEN  Try  ((ElimVar  `n'  THEN  (RWO  "divides\_iff\_rem\_zero"  (-1)    THENM  Reduce  (-1))  THEN  Auto)))\mcdot{}
  THEN  ((CaseNat  3  `n'
                THEN  Auto'
                THEN  Try  ((ElimVar  `n'
                                      THEN  (RWO  "divides\_iff\_rem\_zero"  (-2)    THENM  Reduce  (-2))
                                      THEN  Auto)))
              THEN  CaseNat  4  `n'
              THEN  Auto'
              THEN  Try  ((ElimVar  `n'  THEN  (RWO  "divides\_iff\_rem\_zero"  (-3)    THENM  Reduce  (-3))  THEN  Auto)))
            \mcdot{}
  )

---

Home Index