Proofgold Proposition

∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ (x1 = 0 ⟶ ∀ x3 : ο . x3) ⟶ x0 = mul_SNo x1 x2 ⟶ div_SNo x0 x1 = x2

type
prop

theory
HotG

name
mul_div_SNo_nonzero_eq

proof
PUSRj..

Megalodon
mul_div_SNo_nonzero_eq

proofgold address
TMXcb..^{mul_div_SNo_nonzero_eq}

creator
27837 PrQUS../d57c4..

owner
27837 PrQUS../d57c4..

term root
4c4da..