feat(group_theory/subgroup/basic): Contrapositive of `card_le_one_iff…

…_eq_bot` (#9918)

Adds contrapositive of `card_le_one_iff_eq_bot`.

src/group_theory/subgroup/basic.lean

@@ -479,6 +479,9 @@ end
     (λ x hx, by simpa [subtype.ext_iff] using fintype.card_le_one_iff.1 h ⟨x, hx⟩ 1),
   λ h, by simp [h]⟩
 
+@[to_additive] lemma one_lt_card_iff_ne_bot [fintype H] : 1 < fintype.card H ↔ H ≠ ⊥ :=
+lt_iff_not_ge'.trans (not_iff_not.mpr H.card_le_one_iff_eq_bot)
+
 /-- The inf of two subgroups is their intersection. -/
 @[to_additive "The inf of two `add_subgroups`s is their intersection."]
 instance : has_inf (subgroup G) :=