theorem AdditiveCombinatorics.Finset.card_sub_comm {G : Type u_1} [DecidableEq G] [AddCommGroup G] (A B : Finset G) : (B - A).card = (A - B).card

For finite subsets A, B of an abelian group, the difference sets B - A and A - B have the same cardinality, since one is the negation of the other.

theorem AdditiveCombinatorics.Finset.ruzsa_triangle_inequality {G : Type u_1} [DecidableEq G] [AddCommGroup G] (A B C : Finset G) : A.card * (B - C).card ≤ (A - B).card * (A - C).card

Ruzsa triangle inequality. For any finite subsets A, B, C of an abelian group Z, $$|A| \cdot |B - C| \le |A - B| \cdot |A - C|.$$