---

Step * 1 of Lemma fps-pascal-elim


1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. ¬(1 = 0 ∈ |r|)
⊢ ¬(1 = 0 ∈ PowerSeries(r))
BY
{ xxx(BLemma `fps-non-trivial` THEN Auto)xxx }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  \mneg{}(x  =  y)
5.  \mneg{}(1  =  0)
\mvdash{}  \mneg{}(1  =  0)


By

---

Latex:
xxx(BLemma  `fps-non-trivial`  THEN  Auto)xxx

---

Home Index