---

Step * 1 2 1 of Lemma int_mod_ring_wf


1. n : ℕ+
2. x : ℤ_n
3. y : ℤ_n
⊢ uiff(↑(x mod n =z y mod n);x = y ∈ ℤ_n)
BY
{ TACTIC:(RW assert_pushdownC 0 THENA Try (Complete (Auto))) }

1
1. n : ℕ+
2. x : ℤ_n
3. y : ℤ_n
⊢ uiff((x mod n) = (y mod n) ∈ ℤ;x = y ∈ ℤ_n)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbZ{}\_n
3.  y  :  \mBbbZ{}\_n
\mvdash{}  uiff(\muparrow{}(x  mod  n  =\msubz{}  y  mod  n);x  =  y)


By

---

Latex:
TACTIC:(RW  assert\_pushdownC  0  THENA  Try  (Complete  (Auto)))

---

Home Index