At: prod fin is fin 1 2 6 1 1 8
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)
0
(a2 rem n)
By:
Inst
Thm* a:, n:
. 0(a rem n) & (a rem n) < n
[a2;n]
THEN
ProveProp
Generated subgoals:None
About:
