Proofgold Proposition

∀ x0 x1 x2 . SNo x0 ⟶ (∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ add_SNo (minus_SNo x3) x3 = 0) ⟶ SNo (minus_SNo x0) ⟶ x1 = add_SNo (minus_SNo x0) x2 ⟶ SNo x2 ⟶ SNoLt x2 x0 ⟶ SNo (minus_SNo x2) ⟶ SNoLt x1 0

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_add_SNo_minus_SNo_linv__9__5

proofgold address
TMdGz..^{Conj_add_SNo_minus_SNo_linv__9__5}

creator
35053 PrNpY../8486d..

owner
35061 PrNpY../4fa12..

term root
9f61a..