feat(group_theory/subgroup): eq_bot_of_card_eq (#8413) Companion lemma to eq_top_of_card_eq.
eq_top_of_card_eq