Step
*
1
1
of Lemma
two-factorizations-no-repeats
1. n : ℕ
⊢ no_repeats({x:ℤ| (1 ≤ x) ∧ x < n + 1} filter(λa.(n rem a =z 0);[1, n + 1)))
BY
{ (BLemma `no_repeats_filter` THEN Auto) }
1
1. n : ℕ
⊢ no_repeats({x:ℤ| (1 ≤ x) ∧ x < n + 1} [1, n + 1))
Latex:
Latex:
1.  n  :  \mBbbN{}
\mvdash{}  no\_repeats(\{x:\mBbbZ{}|  (1  \mleq{}  x)  \mwedge{}  x  <  n  +  1\}  ;filter(\mlambda{}a.(n  rem  a  =\msubz{}  0);[1,  n  +  1)))
By
Latex:
(BLemma  `no\_repeats\_filter`  THEN  Auto)
Home
Index