---

Step * 1 1 1 of Lemma eqmod-by-orbits


1. p : ℕ
2. T : Type
⊢ (∀orbit∈[].(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||)) ⇒ (0 ≡ 0 mod p)
BY
{ TACTIC:(Auto THEN Try ((D -1 THEN Auto)) THEN RelRST THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}
2.  T  :  Type
\mvdash{}  (\mforall{}orbit\mmember{}[].(||orbit||  =  1)  \mvee{}  (p  |  ||orbit||))  {}\mRightarrow{}  (0  \mequiv{}  0  mod  p)


By

---

Latex:
TACTIC:(Auto  THEN  Try  ((D  -1  THEN  Auto))  THEN  RelRST  THEN  Auto)

---

Home Index