{A B C : Group} {i : A $-> B} {f : B $-> C} `{IsEmbedding i} (ex : IsExact (Tr (-1)) i f) : i $o (grp_iso_inverse (grp_iso_cxfib ex)) $== subgroup_incl (grp_kernel f). Proof. rapply equiv_ind. 1: exact (isequiv_cxfib ex). intro x. exact (ap (fun y => i y) (eissect _ x)). Defined.
Require Import Basics Types. Require Import Truncations.Core. Require Import WildCat.Core Pointed. Require Import Groups.Group Groups.Subgroup Groups.Kernel. Require Import Homotopy.ExactSequence Modalities.Identity.