{B A : AbGroup} (E : AbSES B A) {s : B $-> E} (h : (projection _) $o s == idmap) : projection_split_iso E h o (inclusion _) == ab_biprod_inl. Proof. intro a. nrapply path_prod'. 2: rapply cx_isexact. lhs nrapply (ap _ (projection_split_to_kernel_beta E h a)). apply eissect. Defined.
Require Import Basics Types Truncations.Core. Require Import HSet WildCat. Require Import Groups.QuotientGroup Groups.ShortExactSequence. Require Import AbelianGroup AbGroups.Biproduct AbHom. Require Import Homotopy.ExactSequence Pointed. Require Import Modalities.ReflectiveSubuniverse.