const In : set set prop term iIn = In infix iIn 2000 2000 const SNo : set prop const SNoLt : set set prop term < = SNoLt infix < 2020 2020 term SNoCutP = \x:set.\y:set.(!z:set.z iIn x -> SNo z) & (!z:set.z iIn y -> SNo z) & !z:set.z iIn x -> !w:set.w iIn y -> z < w const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom SNo_add_SNo_3: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> SNo (x + y + z) axiom add_SNo_3_3_3_Lt1: !x:set.!y:set.!z:set.!w:set.!u:set.SNo x -> SNo y -> SNo z -> SNo w -> SNo u -> (x + y) < z + w -> (x + y + u) < z + w + u axiom add_SNo_com: !x:set.!y:set.SNo x -> SNo y -> x + y = y + x axiom add_SNo_3_2_3_Lt1: !x:set.!y:set.!z:set.!w:set.!u:set.SNo x -> SNo y -> SNo z -> SNo w -> SNo u -> (y + x) < z + w -> (x + u + y) < z + w + u axiom SNoLt_tra: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x < y -> y < z -> x < z const minus_SNo : set set term - = minus_SNo axiom add_SNo_minus_Lt_lem: !x:set.!y:set.!z:set.!w:set.!u:set.!v:set.SNo x -> SNo y -> SNo z -> SNo w -> SNo u -> SNo v -> (x + y + v) < w + u + z -> (x + y + - z) < w + u + - v const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 const SNoR : set set const SNoL : set set var x:set var y:set var z:set var w:set var u:set var v:set var x2:set var y2:set hyp SNo (x * y) hyp !z2:set.z2 iIn SNoL x -> !w2:set.w2 iIn SNoL y -> (z2 * y + x * w2) < x * y + z2 * w2 hyp !z2:set.z2 iIn SNoL x -> !w2:set.w2 iIn SNoR y -> (x * y + z2 * w2) < z2 * y + x * w2 hyp u iIn SNoL x hyp v iIn SNoL y hyp z = u * y + x * v + - u * v hyp SNo (u * y) hyp SNo (x * v) hyp SNo (u * v) hyp x2 iIn SNoL x hyp y2 iIn SNoR y hyp w = x2 * y + x * y2 + - x2 * y2 hyp SNo x2 hyp SNo y2 hyp SNo (x2 * y) hyp SNo (x * y2) claim SNo (x2 * y2) -> z < w