Proofgold Proposition

∀ x0 x1 . SNo x0 ⟶ SNo_min_of (SNoR x0) x1 ⟶ ∀ x2 . SNo x2 ⟶ SNoLt x2 x0 ⟶ SNoLt (add_SNo x0 x0) (add_SNo x1 x2) ⟶ ∃ x3 . and (x3 ∈ SNoL x2) (add_SNo x1 x3 = add_SNo x0 x0)

type
prop

theory
HotG

name
double_SNo_min_1

proof
PUesu..

Megalodon
double_SNo_min_1

proofgold address
TMXv9..^{double_SNo_min_1}

creator
12391 PrGxv../5aab3..

owner
12391 PrGxv../5aab3..

term root
fa7d8..