Nuprl - Proof: hgreater or eq 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hgreater or eq 1

1. m :

2. n :

m) = (n<

(m =

n))

By:	Simpsetp [`bequal`] THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

1 3. nm
  n<m  m = n
2 steps

2 3. n<m  m = n
  nm
1 step

About:

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