Level: Lib Thy Top: 1 3
Hypotheses:

  1. n :

  2. m :

Conclusion:

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

Applied Tactic: Unfold `biject` 0 THENW Auto
Generated subgoals:

1. Inj(n m;(n * m);z.z.1 * m + z.2) Surj(n m;(n * m);z.z.1 * m + z.2)