Nuprl - Proof: least is least2 1 1 1 1

(5steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: least is least2 1 1 1 1

1. p : {p:(

)|

i:

. p(i) }
2. (least i:

. p(i))

3. p(least i:

. p(i))
4.

j:

. j<(least i:

. p(i))

p(j)
5. (least i:

. p(i))

j:

(least i:

. p(i)).

p(j)

By:	SimilarTo: Hyp:-2

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(5steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc