(42steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: sqrt prime irrational 2 1 2

1. p:
2. prime(p)
3. 0 < p
4. m:
5. n:
6. mm = pnn
7. n = 0
8. pnn < 0
n = 0

By: Assert (0mm)

Generated subgoal:

1 0mm1 step

About:
intnatural_numbermultiplyless_thanequal

(42steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc