---

Step * of Lemma sqequal_n_add

∀x,y:Base. ∀n,m:ℕ.  ((x ~n + m y) ⇒ (x ~n y))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN (primNatInd (-1) THEN Auto THEN Try ((Subst ⌜n + 0 ~ n⌝ (-1)⋅ THEN Auto)) THEN BackThruSomeHyp)
   THEN ((BLemma `sqequaln_sqlen` THENA Auto')
         THEN (BLemma `sqle_n_subtype_rel` THENA Auto)
         THEN BLemma `sqlen_sqequaln`⋅
         THEN Auto)⋅) }

1
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

---

Latex:

---

Latex:
\mforall{}x,y:Base.  \mforall{}n,m:\mBbbN{}.    ((x  \msim{}n  +  m  y)  {}\mRightarrow{}  (x  \msim{}n  y))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  (primNatInd  (-1)
              THEN  Auto
              THEN  Try  ((Subst  \mkleeneopen{}n  +  0  \msim{}  n\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto))
              THEN  BackThruSomeHyp)
  THEN  ((BLemma  `sqequaln\_sqlen`  THENA  Auto')
              THEN  (BLemma  `sqle\_n\_subtype\_rel`  THENA  Auto)
              THEN  BLemma  `sqlen\_sqequaln`\mcdot{}
              THEN  Auto)\mcdot{})

---

Home Index