const SNo : set prop const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom add_SNo_com: !x:set.!y:set.SNo x -> SNo y -> x + y = y + x const SNoLt : set set prop term < = SNoLt infix < 2020 2020 var g:set set set var x:set var y:set var z:set var w:set var u:set var v:set hyp !x2:set.!y2:set.SNo x2 -> SNo y2 -> SNo (g x2 y2) hyp !x2:set.!y2:set.!z2:set.!w2:set.SNo x2 -> SNo y2 -> SNo z2 -> SNo w2 -> z2 < x2 -> w2 < y2 -> (g z2 y2 + g x2 w2) < g x2 y2 + g z2 w2 hyp SNo x hyp SNo y hyp SNo z hyp SNo (g x y) hyp SNo w hyp x < w hyp SNo u hyp y < u hyp SNo v hyp z < v hyp SNo (g w y) hyp SNo (g w u) hyp SNo (g x u) hyp SNo (g (g w y + g x u) z) hyp SNo (g (g x y + g w u) z) hyp SNo (g (g w y + g x u) v) hyp SNo (g (g x y + g w u) v) hyp SNo (g w y + g x u) claim SNo (g x y + g w u) -> (g (g x y + g w u) z + g (g w y + g x u) v) < g (g w y + g x u) z + g (g x y + g w u) v