PrintForm Definitions finite sets Sections AutomataTheory Doc

At: rect enumer 1 3 1 1 1 1 1 1 1 1 1 1 1 1 1
1. n:
2. m:
3. a3:
4. 0 a3 < n
5. a4:
6. 0 a4 < m
7. a5:
8. 0 a5 < n
9. a6:
10. 0 a6 < m
11. a3m+a4 = a5m+a6 (nm)

a3 = a5 n
By: Inst Thm* a:, n:, p,q:. Div(a;n;p) Div(a;n;q) p = q [a3m+a4;m;a3;a5]
Generated subgoals:

1 Div(a3m+a4;m;a3)
2 Div(a3m+a4;m;a5)

About:
equalnatural_numberallimpliesintaddmultiply