Proofgold Proposition

∀ x0 . x0 ∈ setminus omega (Sing 0) ⟶ ∀ x1 . nat_p x1 ⟶ ∃ x2 . and (x2 ∈ omega) (∃ x4 . and (x4 ∈ x0) (x1 = add_nat (mul_nat x2 x0) x4))

type
prop

theory
HotG

name
quotient_remainder_nat

proof
PUVXT..

Megalodon
quotient_remainder_nat

proofgold address
TMF8Q..^{quotient_remainder_nat}

creator
29757 PrQUS../fa5e6..

owner
29757 PrQUS../fa5e6..

term root
9215c..