---

Step * 1 1 of Lemma posint_munit_elim


1. a : ℕ+@i
⊢ ∃c:ℕ+. (1 = (a * c) ∈ ℕ+) ⇐⇒ a = 1 ∈ ℤ
BY
{ (((RWH (RevLemmaC `divides_nchar`) 0) THENA Auto)
   THEN Try (((BLemma `mul_bounds_1b`) THEN Auto))
   THEN ((RewriteWith [] ``unit_chars assoced_nelim`` 0) THEN Auto)) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}\msupplus{}@i
\mvdash{}  \mexists{}c:\mBbbN{}\msupplus{}.  (1  =  (a  *  c))  \mLeftarrow{}{}\mRightarrow{}  a  =  1


By

---

Latex:
(((RWH  (RevLemmaC  `divides\_nchar`)  0)  THENA  Auto)
  THEN  Try  (((BLemma  `mul\_bounds\_1b`)  THEN  Auto))
  THEN  ((RewriteWith  []  ``unit\_chars  assoced\_nelim``  0)  THEN  Auto))

---

Home Index