Proofgold Proposition

∀ x0 . SNo x0 ⟶ SNoLt 0 x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ SNoS_ (SNoLev x0) ⟶ SNoLt 0 x2 ⟶ and (SNo (x1 x2)) (mul_SNo x2 (x1 x2) = 1)) ⟶ ∀ x2 . nat_p x2 ⟶ and (∀ x3 . x3 ∈ ap (SNo_recipaux x0 x1 x2) 0 ⟶ and (SNo x3) (SNoLt (mul_SNo x0 x3) 1)) (∀ x3 . x3 ∈ ap (SNo_recipaux x0 x1 x2) 1 ⟶ and (SNo x3) (SNoLt 1 (mul_SNo x0 x3)))

type
prop

theory
HotG

name
SNo_recipaux_lem1

proof
PUewm..

Megalodon
SNo_recipaux_lem1

proofgold address
TMR6o..^{SNo_recipaux_lem1}

creator
27779 PrQUS../a2d6e..

owner
27779 PrQUS../a2d6e..

term root
af615..