Level: Lib Thy Top: 1
Hypotheses:

  1. m :

  2. n :

Conclusion:

0 < (mn)

Applied Tactic: NatInd 2 THENW Auto
Generated subgoals:

1. 0 < (m0)

2. 0 < (mn)