Theorem: logapp-<-0
(defthm logapp-<-0 (implies (logapp-guard size i j) (equal (< (logapp size i j) 0) (< j 0))))
