Proofgold Proposition

∀ x0 x1 . 1 ∈ x0 ⟶ divides_nat x0 x1 ⟶ not (divides_nat x0 (ordsucc x1))

type
prop

theory
HotG

name
nat_1In_not_divides_ordsucc

proof
PUPh4..

Megalodon
nat_1In_not_divides_ordsucc

proofgold address
TMQ1S..^{nat_1In_not_divides_ordsucc}

creator
29757 PrQUS../7bb1f..

owner
29757 PrQUS../7bb1f..

term root
96fff..