const SNo : set prop const minus_SNo : set set term - = minus_SNo axiom SNo_minus_SNo: !x:set.SNo x -> SNo - x const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 axiom SNo_mul_SNo: !x:set.!y:set.SNo x -> SNo y -> SNo (x * y) axiom minus_SNo_invol: !x:set.SNo x -> - - x = x axiom mul_SNo_minus_distrR: !x:set.!y:set.SNo x -> SNo y -> x * - y = - x * y axiom mul_SNo_minus_distrL: !x:set.!y:set.SNo x -> SNo y -> (- x) * y = - x * y claim !x:set.!y:set.SNo x -> SNo y -> (- x) * - y = x * y