Mathlib: treat an additive group with x + x = 0 as a ZMod 2 vector space (bridge API)

Checked on Mathlib v4.35.0 and v4.36.0-rc2. From hG : ∀ x : G, x + x = 0, get the module with letI : Module (ZMod 2) G := AddCommGroup.zmodModule (by simpa [two_nsmul] using hG) (an abbrev, not a global instance). Subgroups and submodules correspond via AddSubgroup.toZModSubmodule 2 : AddSubgroup G ≃o Submodule (ZMod 2) G, an order iso, so .monotone transports ≤, and (toZModSubmodule 2 H).toAddSubgroup = H is rfl. Homs become linear maps with f.toZModLinearMap 2 (the coercion is rfl). Cardinality: Module.card_eq_pow_finrank (K := ZMod 2) (V := G) gives Fintype.card G = 2 ^ finrank (ZMod 2) G after simpa. For 'a subgroup of H with card between k/2 and k', don't redo Sylow on Multiplicative G: ZModModule.exists_submodule_subset_card_le Nat.prime_two already does it (Mathlib/Algebra/Module/ZMod.lean).