const SNo : set prop const ordsucc : set set const Empty : set axiom SNo_1: SNo (ordsucc Empty) const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 axiom nonneg_mul_SNo_Le': !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> Empty <= z -> x <= y -> x * z <= y * z axiom mul_SNo_oneL: !x:set.SNo x -> ordsucc Empty * x = x claim !x:set.!y:set.SNo x -> SNo y -> x <= ordsucc Empty -> Empty <= y -> x * y <= y