Nuprl - Pf rc loop sqrt sqr le

(4steps) PrintForm Definitions Lemmas SquareRootLoop Sections NuprlLIB Doc

At: rc loop sqrt sqr le

a:. a(a)sqr

By: Def of ( < nat > )sqr

Generated subgoal:

1 1. a:
2. b:
aaa

About:

(4steps) PrintForm Definitions Lemmas SquareRootLoop Sections NuprlLIB Doc