---

Step * 1 1 1 of Lemma two-factorizations-no-repeats


1. n : ℕ
⊢ no_repeats({x:ℤ| (1 ≤ x) ∧ x < n + 1} ;[1, n + 1))
BY
{ (InstLemma `no_repeats_from-upto` [⌜1⌝;⌜n + 1⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  no\_repeats(\{x:\mBbbZ{}|  (1  \mleq{}  x)  \mwedge{}  x  <  n  +  1\}  ;[1,  n  +  1))


By

---

Latex:
(InstLemma  `no\_repeats\_from-upto`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}n  +  1\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index