Proofgold Proposition

∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ not (and (x0 = 0) (x1 = 0)) ⟶ ∀ x2 : ο . (∀ x3 . and (and (int_lin_comb x0 x1 x3) (SNoLt 0 x3)) (∀ x4 . int_lin_comb x0 x1 x4 ⟶ SNoLt 0 x4 ⟶ SNoLe x3 x4) ⟶ x2) ⟶ x2

type
prop

theory
HotG

name
least_pos_int_lin_comb_ex

proof
PUVXT..

Megalodon
least_pos_int_lin_comb_ex

proofgold address
TMZuE..^{least_pos_int_lin_comb_ex}

creator
29757 PrQUS../e1e56..

owner
29757 PrQUS../e1e56..

term root
adb37..