theorem triangle_equality {F : Type u_1} [Field F] (v : AddValuation F (WithTop ℤ)) {x y : F} (h : v x ≠ v y) : v (x + y) = min (v x) (v y)

theorem addval_ne_top {F : Type u_1} [Field F] (v : AddValuation F (WithTop ℤ)) {x : F} (hx : x ≠ 0) : v x ≠ ⊤

theorem ne_zero_of_val_coe {F : Type u_1} [Field F] {v : AddValuation F (WithTop ℤ)} {x : F} {a : ℤ} (h : v x = ↑a) : x ≠ 0

theorem addval_mul_coe {F : Type u_1} [Field F] (v : AddValuation F (WithTop ℤ)) {x y : F} {a b : ℤ} (ha : v x = ↑a) (hb : v y = ↑b) : v (x * y) = ↑(a + b)

theorem addval_inv_coe {F : Type u_1} [Field F] (v : AddValuation F (WithTop ℤ)) {x : F} {a : ℤ} (h : v x = ↑a) : v x⁻¹ = ↑(-a)

theorem addval_npow_coe {F : Type u_1} [Field F] (v : AddValuation F (WithTop ℤ)) (n : ℕ) {x : F} {a : ℤ} (h : v x = ↑a) : v (x ^ n) = ↑(↑n * a)

theorem addval_zpow_coe {F : Type u_1} [Field F] (v : AddValuation F (WithTop ℤ)) {x : F} {a : ℤ} (h : v x = ↑a) (n : ℤ) : v (x ^ n) = ↑(n * a)

theorem addval_prod {F : Type u_1} [Field F] {n : ℕ} (v : AddValuation F (WithTop ℤ)) (f : Fin n → F) : v (∏ j : Fin n, f j) = ∑ j : Fin n, v (f j)

theorem exists_nat_large_avoiding (a : ℤ) (ha : a < 0) (c : ℤ) (bad : Finset ℕ) : ∃ (N : ℕ), 0 < N ∧ ↑N * a < c ∧ N ∉ bad

theorem build_neg_element_from_seps {F : Type u_1} [Field F] (m : ℕ) (vlast : AddValuation F (WithTop ℤ)) (vi : Fin m → AddValuation F (WithTop ℤ)) (sep : Fin m → F) (hsep_ne : ∀ (i : Fin m), sep i ≠ 0) (hsep_last : ∀ (i : Fin m), 0 ≤ vlast (sep i)) (hsep_neg : ∀ (i : Fin m), (vi i) (sep i) < 0) : ∃ (s : F), s ≠ 0 ∧ 0 ≤ vlast s ∧ ∀ (i : Fin m), (vi i) s < 0

theorem val_prod_zpow_kronecker {F : Type u_1} [Field F] {m : ℕ} (v : AddValuation F (WithTop ℤ)) (t' : Fin m → F) (c : Fin m → ℤ) (i : Fin m) (ht'_ne : ∀ (j : Fin m), t' j ≠ 0) (ht' : ∀ (j : Fin m), v (t' j) = ↑(if i = j then 1 else 0)) : v (∏ j : Fin m, t' j ^ (-c j)) = ↑(-c i)

theorem construct_tn {F : Type u_1} [Field F] (m : ℕ) (v : Fin (m + 1) → AddValuation F (WithTop ℤ)) (hv_surj : ∀ (i : Fin (m + 1)), ∃ (u : F), (v i) u = ↑1) (hv_incomp : ∀ (i j : Fin (m + 1)), i ≠ j → ¬∀ (x : F), 0 ≤ (v i) x → 0 ≤ (v j) x) (t' : Fin m → F) (ht' : ∀ (i j : Fin m), (v i.castSucc) (t' j) = ↑(if i = j then 1 else 0)) : ∃ (tn : F), (v (Fin.last m)) tn = ↑1 ∧ ∀ (i : Fin m), (v i.castSucc) tn = ↑0

theorem independence_of_valuations {F : Type u_1} [Field F] (n : ℕ) (v : Fin n → AddValuation F (WithTop ℤ)) (hv_surj : ∀ (i : Fin n), ∃ (u : F), (v i) u = ↑1) (hv_incomp : ∀ (i j : Fin n), i ≠ j → ¬∀ (x : F), 0 ≤ (v i) x → 0 ≤ (v j) x) : ∃ (t : Fin n → F), ∀ (i j : Fin n), (v i) (t j) = ↑(if i = j then 1 else 0)