theorem zpow_inj_prime {p : ℕ} [hp : Fact (Nat.Prime p)] {a b : ℤ} (h : ↑p ^ a = ↑p ^ b) : a = b

theorem val_neg_implies_norm_gt_one {p : ℕ} [hp : Fact (Nat.Prime p)] {a : ℚ_[p]} (h : a.valuation < 0) : 1 < ‖a‖

theorem ultra3_padic {p : ℕ} [hp : Fact (Nat.Prime p)] {a b c : ℚ_[p]} (hb : ‖b‖ < ‖a‖) (hc : ‖c‖ < ‖a‖) : ‖a + b + c‖ = ‖a‖

theorem ultra4_padic {p : ℕ} [hp : Fact (Nat.Prime p)] {a b c d : ℚ_[p]} (hb : ‖b‖ < ‖a‖) (hc : ‖c‖ < ‖a‖) (hd : ‖d‖ < ‖a‖) : ‖a + b + c + d‖ = ‖a‖

theorem rhs_norm_le_one {p : ℕ} [hp : Fact (Nat.Prime p)] {a₂ a₄ a₆ x : ℚ_[p]} (hn₂ : ‖a₂‖ ≤ 1) (hn₄ : ‖a₄‖ ≤ 1) (hn₆ : ‖a₆‖ ≤ 1) (hx_le : ‖x‖ ≤ 1) : ‖x ^ 3 + a₂ * x ^ 2 + a₄ * x + a₆‖ ≤ 1

theorem rhs_norm_eq_cube {p : ℕ} [hp : Fact (Nat.Prime p)] {a₂ a₄ a₆ x : ℚ_[p]} (hn₂ : ‖a₂‖ ≤ 1) (hn₄ : ‖a₄‖ ≤ 1) (hn₆ : ‖a₆‖ ≤ 1) (hx_gt : 1 < ‖x‖) : ‖x ^ 3 + a₂ * x ^ 2 + a₄ * x + a₆‖ = ‖x‖ ^ 3

theorem weierstrass_valuation_bound_proof {p : ℕ} [hp : Fact (Nat.Prime p)] {W : WeierstrassCurve ℚ} [W.IsElliptic] (hc : 0 ≤ ((algebraMap ℚ ℚ_[p]) W.a₁).valuation ∧ 0 ≤ ((algebraMap ℚ ℚ_[p]) W.a₂).valuation ∧ 0 ≤ ((algebraMap ℚ ℚ_[p]) W.a₃).valuation ∧ 0 ≤ ((algebraMap ℚ ℚ_[p]) W.a₄).valuation ∧ 0 ≤ ((algebraMap ℚ ℚ_[p]) W.a₆).valuation) {x y : ℚ_[p]} (h : (W.baseChange ℚ_[p]).toAffine.Nonsingular x y) (hni : ¬(0 ≤ x.valuation ∧ 0 ≤ y.valuation)) : y ≠ 0 ∧ 1 ≤ x.valuation - y.valuation