---

Step * of Lemma no_repeats-residues-mod

∀[n:ℕ]. no_repeats(residue(n);residues-mod(n))
BY
{ (Auto
   THEN Assert ⌜no_repeats(ℤ;residues-mod(n))⌝⋅
   THEN Try (((InstLemma `no_repeats-subtype` [⌜ℤ⌝;⌜residue(n)⌝]⋅ THENA Auto) THEN BHyp -1  THEN Auto)⋅)) }

1
.....assertion..... 
1. n : ℕ
⊢ no_repeats(ℤ;residues-mod(n))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  no\_repeats(residue(n);residues-mod(n))


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}no\_repeats(\mBbbZ{};residues-mod(n))\mkleeneclose{}\mcdot{}
  THEN  Try  (((InstLemma  `no\_repeats-subtype`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}residue(n)\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  BHyp  -1    THEN  Auto)
                      \mcdot{}))

---

Home Index