Proofgold Proposition

∀ x0 x1 . x1 ∈ omega ⟶ ∀ x2 . nat_p x2 ⟶ x0 ∈ add_SNo x1 x2 ⟶ or (x0 ∈ x1) (add_SNo x0 (minus_SNo x1) ∈ x2)

type
prop

theory
HotG

name
add_SNo_omega_In_cases

proof
PUMXD..

Megalodon
add_SNo_omega_In_cases

proofgold address
TMNFe..^{add_SNo_omega_In_cases}

creator
12443 PrGxv../85fbf..

owner
12443 PrGxv../85fbf..

term root
3eee9..