Nuprl - Pf divide_wf 1 2 1 1 1

1. a:
2. n:

0 < n+n(a n)

By: Assert (0n(a n)+(a rem n) & n(a n)+(a rem n) < n+n(a n))

Generated subgoals:

1 0n(a n)+(a rem n) & n(a n)+(a rem n) < n+n(a n)

2 3. 0n(a n)+(a rem n) & n(a n)+(a rem n) < n+n(a n)
0 < n+n(a n)

About:

1	`0n(a n)+(a rem n) & n(a n)+(a rem n) < n+n(a n)`
2	3. `0n(a n)+(a rem n) & n(a n)+(a rem n) < n+n(a n)` `0 < n+n(a n)`