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 mul_SNo_minus_distrL: !x:set.!y:set.SNo x -> SNo y -> (- x) * y = - x * y axiom mul_SNo_com: !x:set.!y:set.SNo x -> SNo y -> x * y = y * x claim !x:set.!y:set.SNo x -> SNo y -> x * - y = - x * y