Example. [isa-001Q]

We can prove a theorem about our factorial definition:

theorem factorial_mult: "factorial n * factorial m ≤ factorial (n + m)"

Solution.