Nuprl - Pf ndiff_ndiff_eq_imin

(6steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: ndiff ndiff eq imin

a,b:. (a -- (a -- b)) = imin(a;b)

By: UnivCD THEN Unfold `ndiff` 0 THEN ArithSimp 0

Generated subgoal:

1 1. a:
2. b:
imax(a+-imax(a+-b;0);0) = imin(a;b)

About:

(6steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc