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