Level: Lib Thy Top: 1 2
Hypotheses:

  1. n :

  2. m :

  3. z : n m

Conclusion:

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

Applied Tactic: D 3 THEN Reduce 0
Generated subgoals:

1. z1 * m + z2 < n * m