proposition: Lemma ab_biprod_assoc {A B C : AbGroup} : ab_biprod A (ab_biprod B C) $<~> ab_biprod (ab_biprod A B) C.
proof: Proof. snrapply Build_GroupIsomorphism'. - apply equiv_prod_assoc. - unfold IsSemiGroupPreserving; reflexivity. Defined.
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse