Proofgold Proposition

∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ not (and (x0 = 0) (x1 = 0)) ⟶ ∀ x2 . iff (gcd_reln x0 x1 x2) (and (and (int_lin_comb x0 x1 x2) (SNoLt 0 x2)) (∀ x3 . int_lin_comb x0 x1 x3 ⟶ SNoLt 0 x3 ⟶ SNoLe x2 x3))

type
prop

theory
HotG

name
BezoutThm

proof
PUVXT..

Megalodon
BezoutThm

proofgold address
TMR5m..^BezoutThm

creator
29757 PrQUS../8cdcb..

owner
29757 PrQUS../8cdcb..

term root
01513..