At: fun enumer 1 2 1 2 2 1 2 1 1 1 1 1 1 2 1 1 1
1. n: 
2. m: 
3. 0 < m
4. f: ((m-1)
n)(n
m-1)
5. Bij((m-1)n; (nm-1); f)
6. 
n = 0
7. f1: n
(nm-1)(nm)
8. 
a1,a2:(n(nm-1)). f1(a1) = f1(a2) 
(n
(nm-1)) 
a1 = a2
9. a1: mn
10. a2: mn
11. f1( < a1(m-1),f(a1) > ) = f1( < a2(m-1),f(a2) > )
12. a1(m-1) = a2(m-1)
13. f(a1) = f(a2)
14. x: m
15. x = m-1 m
a1(x) = a2(x)
By: RWH (HypC 15) 0
Generated subgoals:None
About:
