Proofgold Proposition

∀ x0 . x0 ∈ setminus omega (Sing 0) ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ omega) (∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x1 = add_nat (mul_nat x3 x0) x5) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2

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..