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

At: imin assoc

a,b,c:. imin(a;imin(b;c)) = imin(imin(a;b);c)
By:
UnivCD
THEN
BackThru Thm* i,j:. i = j -i = -j
THEN
RewriteWith [] [ Thm* a,b:. -imin(a;b) = imax(-a;-b)] 0
Generated subgoal:

11. a:
2. b:
3. c:
imax(-a;imax(-b;-c)) = imax(imax(-a;-b);-c)

About:
intminusequalall

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