Proofgold Proposition

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo x0 (minus_SNo x1) = minus_SNo (mul_SNo x0 x1)

type
prop

theory
HotG

name
mul_SNo_minus_distrR

proof
PUUxZ..

Megalodon
mul_minus_SNo_distrR

proofgold address
TMYse..^{mul_minus_SNo_distrR}

creator
8219 Pr6Pc../7d00b..

owner
8219 Pr6Pc../7d00b..

term root
ab775..