---

Step * of Lemma nsub2-flip

∀[x,y:ℕ2].  uiff((1 - x) = y ∈ ℕ2;x = (1 - y) ∈ ℕ2)
BY
{ (RepeatFor 2 (((D 0 THENA Auto) THEN IntSegCases (-1) THEN Reduce 0)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbN{}2].    uiff((1  -  x)  =  y;x  =  (1  -  y))


By

---

Latex:
(RepeatFor  2  (((D  0  THENA  Auto)  THEN  IntSegCases  (-1)  THEN  Reduce  0))  THEN  Auto)

---

Home Index