At: prod fin is fin 1 2 6 1 1 1 1 6
1. T: Type
2. t: T
3. n: 
4. f: n
T
5. 
a1,a2:n. f(a1) = f(a2) 
a1 = a2
6. Surj(n; T; f)
7. n > 0
8. a1: (n
n)
9. a2: (nn)
10. f(a1 
n) = f(a2 n)
11. f(a1 rem n) = f(a2 rem n)
12. (a1 n) = (a2 n) 
n
(a1 rem n) < n
By:
Inst
Thm* a:, n:
. 0
(a rem n) & (a rem n) < n
[a1;n]
THEN
ProveProp
Generated subgoals:None
About:
