Proofgold Proposition

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe 1 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) (minus_SNo 1)

type
prop

theory
HotG

name
minus_SNo_Le_swap_1

proof
PUY2k..

Megalodon
minus_SNo_Le_swap_1

proofgold address
TMcQv..^{minus_SNo_Le_swap_1}

creator
16784 PrGxv../474df..

owner
16784 PrGxv../474df..

term root
909df..