PrintForm Definitions finite sets Sections AutomataTheory Doc

At: prod fin is fin 1 2 6 2 1 1 1 3 2
1. T: Type
2. t: T
3. n:
4. f: nT
5. Inj(n; T; f)
6. b:T. a:n. f(a) = b
7. n > 0
8. b1: T
9. b2: T
10. a: n
11. f(a) = b1
12. a1: n
13. f(a1) = b2

f((an+a1) rem n) = b2
By:
Inst Thm* a,b:, n:. ((a+bn) rem n) = (a rem n) [a1;a;n]
THEN
Inst Thm* a:, n:. a < n (a rem n) = a [a1;n]
Generated subgoal:

114. ((a1+an) rem n) = (a1 rem n)
15. (a1 rem n) = a1
f((an+a1) rem n) = b2

About:
equalapplyremainderaddmultiply
universefunctionnatural_numberallexists