(6steps) PrintForm Lemmas int 2 Sections StandardLIB Doc

At: mul preserves lt 1 1
1. a:
2. b:
3. a < b
4. n:
5. 0 < n
6. 1 = n

na < nb
By: RevHypSubst 6 0
Generated subgoals:

None

About:
intnatural_numbermultiplyless_thanequal

(6steps) PrintForm Lemmas int 2 Sections StandardLIB Doc