theorem card_field_prime_pow {α : Type u_1} [Field α] [Fintype α] : IsPrimePow (Fintype.card α)

theorem two_le_card_field {α : Type u_1} [Field α] [Fintype α] : 2 ≤ Fintype.card α

theorem exists_grower {α : Type u_1} [Field α] [Fintype α] [DecidableEq α] (A : Finset α) : ∃ (a : α), a ≠ 0 ∧ ↑(A + a • A).card ≥ ↑(min (A.card ^ 2) (Fintype.card α)) / 2

theorem GUS (p : ℕ) [Fact (Nat.Prime p)] (A : Finset (ZMod p)) : ↑(3 • A ^ 2 - 3 • A ^ 2).card ≥ ↑(min (A.card ^ 2) p) / 2