{G : Group} (g : G) := cyclic_subgroup_from_unit (unit_name g). Global Instance commutative_cyclic_subgroup {G : Group} (gen : Unit -> G) : Commutative (@group_sgop (cyclic_subgroup_from_unit gen)). Proof. intros h k. destruct h as [h H]; cbn in H. destruct k as [k K]; cbn in K. strip_truncations. apply (equiv_ap_isembedding (subgroup_incl _) _ _)^-1. cbn. induction H as [h [[] p]| |h1 h2 H1 H2 IHH1 IHH2]. - induction p. induction K as [k [[] q]| |k1 k2 K1 K2 IHK1 IHK2]. + induction q. reflexivity. + apply centralizer_unit. + srapply (issubgroup_in_op_inv (H:=centralizer (gen tt))); assumption. - symmetry; apply centralizer_unit. - symmetry. srapply (issubgroup_in_op_inv (H:=centralizer k)); unfold centralizer; symmetry; assumption. Defined.
Require Import Basics Types Truncations.Core. Require Import HFiber AbelianGroup.