proposition: Lemma abses_twist_directsum `{Funext} {A B : AbGroup} (E F G : AbSES B A) : AbSESMorphism (abses_direct_sum (abses_direct_sum E F) G) (abses_direct_sum (abses_direct_sum G F) E).
proof: Proof. snrapply Build_AbSESMorphism. 1,2,3: exact ab_biprod_twist. all: reflexivity. Defined.
imports: Basics Types Truncations.Core Pointed.Core WildCat.Core Homotopy.ExactSequence AbGroups.AbelianGroup AbSES.Core AbGroups.Biproduct