Level: Lib Thy Top: 1
Hypotheses:

  1. n :

  2. m :

Conclusion:

f:(n m) (n * m). Bij(n m;(n * m);f)

Applied Tactic: With z.z.1 * m + z.2 (D 0) THENW Auto
Generated subgoals:

1. 0 z.1 * m + z.2

2. z.1 * m + z.2 < n * m

3. Bij(n m;(n * m);z.z.1 * m + z.2)