theorem sub_le_add {α : Type u_1} [DecidableEq α] (A : Finset α) (B : Finset α) [AddCommGroup α] : ↑(A - B).card ≤ ↑(A + B).card ^ 3 / (↑A.card * ↑B.card)

theorem card_of_inv {α : Type u_1} [DecidableEq α] (A : Finset α) [GroupWithZero α] (a : α) (h : a ≠ 0) : (a • A).card = A.card

theorem neg_inter_distrib {α : Type u_1} [DecidableEq α] (A : Finset α) (B : Finset α) [InvolutiveNeg α] : -A ∩ -B = -(A ∩ B)

theorem add_smul_subset_smul_add_smul {α : Type u_1} [DecidableEq α] (A : Finset α) [CommSemiring α] (a : α) (b : α) : (a + b) • A ⊆ a • A + b • A

theorem sub_smul_subset_smul_sub_smul {α : Type u_1} [DecidableEq α] (A : Finset α) [CommRing α] (a : α) (b : α) : (a - b) • A ⊆ a • A - b • A

theorem add_of_large_intersection {α : Type u_1} [DecidableEq α] (A : Finset α) (B : Finset α) (C : Finset α) [AddCommGroup α] (h : (A ∩ C).Nonempty) : ↑(B + C).card ≤ ↑(B + A).card * ↑(C + C).card / ↑(A ∩ C).card

theorem triple_add {α : Type u_1} [DecidableEq α] (A : Finset α) (B : Finset α) (C : Finset α) [AddCommGroup α] : ↑(A + B + C).card ≤ ↑(C + A).card * ↑(A + B).card ^ 8 / (↑A.card ^ 6 * ↑B.card ^ 2)

theorem additive_mul_eq {α : Type u_1} [DecidableEq α] (A : Finset α) [Field α] (C : α) (h : C ≠ 0) : E[A, C • A] = (Finset.filter (fun (x : (α × α) × α × α) => x.1.1 + C * x.1.2 = x.2.1 + C * x.2.2) ((A ×ˢ A) ×ˢ A ×ˢ A)).card