{B A : AbGroup} (E : AbSES B A) {s : B $-> E} (h : (projection _) $o s == idmap) : (projection_split_to_kernel E h) $o (inclusion _) == grp_cxfib cx_isexact. Proof. intro a. apply path_sigma_hprop; cbn. apply grp_cancelL1. refine (ap (fun x => - s x) _ @ _). 1: rapply cx_isexact. exact (ap _ (grp_homo_unit _) @ negate_mon_unit). 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.