α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
⊢ card (A / C⁻¹) * card B ≤ card (A / B) * card (B / C⁻¹)
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
⊢ card (A * C) * card B ≤ card (A / B) * card (B * C)
rw [← div_inv_eq_mul, ← div_inv_eq_mul B]
no goals
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
⊢ card (A / C⁻¹) * card B ≤ card (A / B) * card (B / C⁻¹)
exact card_div_mul_le_card_div_mul_card_div _ _ _