---

Step * 1 of Lemma sqequal_n_add


1. x : Base
2. y : Base
3. n : ℕ
4. m : ℤ
5. 0 < m
6. (x ~n + (m - 1) y) ⇒ (x ~n y)
7. x ~n + m y
⊢ y ~(n + (m - 1)) + 1 x
BY
{ (BLemma `sqequaln_symm` THEN Auto THEN NthHypSq (-1) THEN EqCD THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  x  :  Base
2.  y  :  Base
3.  n  :  \mBbbN{}
4.  m  :  \mBbbZ{}
5.  0  <  m
6.  (x  \msim{}n  +  (m  -  1)  y)  {}\mRightarrow{}  (x  \msim{}n  y)
7.  x  \msim{}n  +  m  y
\mvdash{}  y  \msim{}(n  +  (m  -  1))  +  1  x


By

---

Latex:
(BLemma  `sqequaln\_symm`  THEN  Auto  THEN  NthHypSq  (-1)  THEN  EqCD  THEN  Auto)\mcdot{}

---

Home Index