At: fun enumer 1 2 1 1 1 1 1 1 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. a1: mn
8. a2: mn
9. a1(0) = a2(0)
10. 0 
a1(0) < (nm)
11. x: m
a1(x) = a2(x)
By: Inst
Thm* 
m:
. (0m) = 0
[m]
Generated subgoals:None
About:
