diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean
index 2cfdfad..a302cfa 100644
--- a/algebra/exact_couple.hlean
+++ b/algebra/exact_couple.hlean
@@ -671,8 +671,8 @@ namespace pointed
   definition homotopy_group_conn_nat_functor (n : ℕ) {A B : Type*[1]} (f : A →* B) :
     homotopy_group_conn_nat n A →g homotopy_group_conn_nat n B :=
   begin
-    cases n with n, { apply trivial_homomorphism },
-    cases n with n, { apply trivial_homomorphism },
+    cases n with n, { apply group.trivial_homomorphism },
+    cases n with n, { apply group.trivial_homomorphism },
     exact π→g[n+2] f
   end
 
diff --git a/algebra/exactness.hlean b/algebra/exactness.hlean
index 8e78fca..b90bdd9 100644
--- a/algebra/exactness.hlean
+++ b/algebra/exactness.hlean
@@ -243,37 +243,6 @@ definition is_contr_left_of_is_short_exact {A B : Type} {C : Type*} {f : A → B
   (H : is_short_exact f g) (HB : is_contr B) (a₀ : A) : is_contr A :=
 is_contr_of_is_embedding f (is_short_exact.is_emb H) _ a₀
 
-/- TODO: move and remove other versions -/
-
-  definition is_surjective_qg_map {A : Group} (N : property A) [is_normal_subgroup A N] :
-    is_surjective (qg_map N) :=
-  begin
-    intro x, induction x,
-    fapply image.mk,
-    exact a, reflexivity,
-    apply is_prop.elimo
-  end
-
-  definition is_surjective_ab_qg_map {A : AbGroup} (N : property A) [is_normal_subgroup A N] :
-    is_surjective (ab_qg_map N) :=
-  is_surjective_ab_qg_map _
-
-  definition qg_map_eq_one {A : Group} {K : property A} [is_normal_subgroup A K] (g : A)
-      (H : g ∈ K) :
-    qg_map K g = 1 :=
-  begin
-    apply set_quotient.eq_of_rel,
-    have e : g * 1⁻¹ = g,
-    from calc
-      g * 1⁻¹ = g * 1 : one_inv
-        ...   = g : mul_one,
-    exact transport (λx, K x) e⁻¹ H
-  end
-
-  definition ab_qg_map_eq_one {A : AbGroup} {K : property A} [is_subgroup A K] (g : A)
-      (H : g ∈ K) :
-    ab_qg_map K g = 1 :=
-  ab_qg_map_eq_one g H
 
 definition is_short_exact_normal_subgroup {G : Group} (S : property G) [is_normal_subgroup G S] :
   is_short_exact (incl_of_subgroup S) (qg_map S) :=
@@ -287,4 +256,5 @@ begin
   { exact is_surjective_qg_map S },
 end
 
+
 end algebra
diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean
index acc277a..257a620 100644
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@@ -183,6 +183,10 @@ definition left_module_AddAbGroup_of_LeftModule [instance] {R : Ring} (M : LeftM
   left_module R (AddAbGroup_of_LeftModule M) :=
 LeftModule.struct M
 
+definition left_module_AddAbGroup_of_LeftModule2 [instance] {R : Ring} (M : LeftModule R) :
+  left_module R (Group_of_AbGroup (AddAbGroup_of_LeftModule M)) :=
+LeftModule.struct M
+
 definition left_module_of_ab_group {G : Type} [gG : add_ab_group G] {R : Type} [ring R]
   (smul : R → G → G)
   (h1 : Π (r : R) (x y : G), smul r (x + y) = (smul r x + smul r y))
@@ -423,6 +427,15 @@ section
     (g : B →lm C)
     (h : @is_short_exact A B C f g)
 
+  structure five_exact_mod (A B C D E : LeftModule R) :=
+    (f₁ : A →lm B)
+    (f₂ : B →lm C)
+    (f₃ : C →lm D)
+    (f₄ : D →lm E)
+    (h₁ : @is_exact A B C f₁ f₂)
+    (h₂ : @is_exact B C D f₂ f₃)
+    (h₃ : @is_exact C D E f₃ f₄)
+
   local abbreviation g_of_lm := @group_homomorphism_of_lm_homomorphism
   definition short_exact_mod_of_is_exact {X A B C Y : LeftModule R}
     (k : X →lm A) (f : A →lm B) (g : B →lm C) (l : C →lm Y)
@@ -610,4 +623,5 @@ group_isomorphism_of_lm_isomorphism φ
 
 end int
 
+
 end left_module
diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean
index bdc433d..45c0e8e 100644
--- a/algebra/quotient_group.hlean
+++ b/algebra/quotient_group.hlean
@@ -150,7 +150,8 @@ namespace group
   definition ab_qg_map {G : AbGroup} (N : property G) [is_subgroup G N] : G →g quotient_ab_group N :=
   @qg_map _ N (is_normal_subgroup_ab _)
 
- definition is_surjective_ab_qg_map {A : AbGroup} (N : property A) [is_subgroup A N] : is_surjective (ab_qg_map N) :=
+  definition is_surjective_qg_map {A : Group} (N : property A) [is_normal_subgroup A N] :
+    is_surjective (qg_map N) :=
   begin
     intro x, induction x,
     fapply image.mk,
@@ -158,6 +159,10 @@ namespace group
     apply is_prop.elimo
   end
 
+  definition is_surjective_ab_qg_map {A : AbGroup} (N : property A) [is_subgroup A N] :
+    is_surjective (ab_qg_map N) :=
+  @is_surjective_qg_map _ _ _
+
   namespace quotient
     notation `⟦`:max a `⟧`:0 := qg_map _ a
   end quotient
@@ -165,25 +170,20 @@ namespace group
   open quotient
   variables {N N'}
 
-  definition qg_map_eq_one (g : G) (H : N g) : qg_map N g = 1 :=
+  definition qg_map_eq_one {A : Group} {K : property A} [is_normal_subgroup A K] (g : A)
+      (H : g ∈ K) : qg_map K g = 1 :=
   begin
-    apply eq_of_rel,
-      have e : (g * 1⁻¹ = g),
-      from calc
+    apply set_quotient.eq_of_rel,
+    have e : g * 1⁻¹ = g,
+    from calc
       g * 1⁻¹ = g * 1 : one_inv
         ...   = g : mul_one,
-    unfold quotient_rel, rewrite e, exact H
+    exact transport (λx, K x) e⁻¹ H
   end
 
-  definition ab_qg_map_eq_one {K : property A} [is_subgroup A K] (g :A) (H : K g) : ab_qg_map K g = 1 :=
-  begin
-    apply eq_of_rel,
-      have e : (g * 1⁻¹ = g),
-      from calc
-      g * 1⁻¹ = g * 1 : one_inv
-        ...   = g : mul_one,
-    unfold quotient_rel, xrewrite e, exact H
-  end
+  definition ab_qg_map_eq_one {A : AbGroup} {K : property A} [is_subgroup A K] (g : A) (H : g ∈ K) :
+    ab_qg_map K g = 1 :=
+  @qg_map_eq_one _ _ _ g H
 
    --- there should be a smarter way to do this!! Please have a look, Floris.
   definition rel_of_qg_map_eq_one (g : G) (H : qg_map N g = 1) : g ∈ N :=
@@ -454,16 +454,14 @@ namespace group
 
 definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_ab_group (kernel f) →g B :=
   begin
-    unfold quotient_ab_group,
-    fapply @quotient_group_elim A B _ (@is_normal_subgroup_ab _ (kernel f) _) f,
+    apply quotient_ab_group_elim f,
     intro a, intro p, exact p
   end
 
 definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) :
   kernel_quotient_extension f ∘ ab_qg_map (kernel f) ~ f :=
   begin
-    intro a,
-    apply @quotient_group_compute _ _ _ (@is_normal_subgroup_ab _ (kernel f) _)
+    intro a, reflexivity
   end
 
 definition is_embedding_kernel_quotient_extension {A B : AbGroup} (f : A →g B) :
@@ -474,7 +472,7 @@ definition is_embedding_kernel_quotient_extension {A B : AbGroup} (f : A →g B)
     note H := is_surjective_ab_qg_map (kernel f) x,
     induction H, induction p,
     intro q,
-    apply @qg_map_eq_one _ _ (@is_normal_subgroup_ab _ (kernel f) _),
+    apply ab_qg_map_eq_one,
     refine _ ⬝ q,
     symmetry,
     rexact kernel_quotient_extension_triangle f a
@@ -698,6 +696,27 @@ namespace group
     exact ap set_quotient.class_of (p g)
   end
 
+  definition quotient_group_isomorphism_quotient_group [constructor] (φ : G ≃g H)
+    (h : Πg, g ∈ R ↔ φ g ∈ S) : quotient_group R ≃g quotient_group S :=
+  begin
+    refine isomorphism.MK (quotient_group_functor φ (λg, iff.mp (h g)))
+      (quotient_group_functor φ⁻¹ᵍ (λg gS, iff.mpr (h _) (transport S (right_inv φ g)⁻¹ gS))) _ _,
+    { refine quotient_group_functor_compose _ _ _ _ ⬝hty
+             quotient_group_functor_homotopy _ _ proof right_inv φ qed ⬝hty
+             quotient_group_functor_gid },
+    { refine quotient_group_functor_compose _ _ _ _ ⬝hty
+             quotient_group_functor_homotopy _ _ proof left_inv φ qed ⬝hty
+             quotient_group_functor_gid }
+  end
+
+  definition is_equiv_qg_map {G : Group} (H : property G) [is_normal_subgroup G H]
+    (H₂ : Π⦃g⦄, g ∈ H → g = 1) : is_equiv (qg_map H) :=
+  set_quotient.is_equiv_class_of _ (λg h r, eq_of_mul_inv_eq_one (H₂ r))
+
+  definition quotient_group_isomorphism [constructor] {G : Group} (H : property G)
+    [is_normal_subgroup G H] (h : Πg, g ∈ H → g = 1) : quotient_group H ≃g G :=
+  (isomorphism.mk _ (is_equiv_qg_map H h))⁻¹ᵍ
+
 end group
 
 namespace group
@@ -735,4 +754,16 @@ namespace group
     quotient_ab_group_functor φ hφ ~ quotient_ab_group_functor ψ hψ :=
   @quotient_group_functor_homotopy G H R _ S _ ψ φ hψ hφ p
 
+  definition is_equiv_ab_qg_map {G : AbGroup} (H : property G) [is_subgroup G H]
+    (h : Π⦃g⦄, g ∈ H → g = 1) : is_equiv (ab_qg_map H) :=
+  proof @is_equiv_qg_map G H (is_normal_subgroup_ab _) h qed
+
+  definition ab_quotient_group_isomorphism [constructor] {G : AbGroup} (H : property G)
+    [is_subgroup G H] (h : Πg, H g → g = 1) : quotient_ab_group H ≃g G :=
+  (isomorphism.mk _ (is_equiv_ab_qg_map H h))⁻¹ᵍ
+
+  definition quotient_ab_group_isomorphism_quotient_ab_group [constructor] (φ : G ≃g H)
+    (h : Πg, g ∈ R ↔ φ g ∈ S) : quotient_ab_group R ≃g quotient_ab_group S :=
+  @quotient_group_isomorphism_quotient_group _ _ _ _ _ _ φ h
+
 end group
diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean
index ec3bdcf..4fb98cd 100644
--- a/algebra/spectral_sequence.hlean
+++ b/algebra/spectral_sequence.hlean
@@ -140,7 +140,16 @@ namespace spectral_sequence
     Einf c (n, s) ≃lm E' n s :=
   E_isomorphism0 c (λr Hr, H1 r) (λr Hr, H2 r)
 
-  /- we call a spectral sequence normal if it is a first-quadrant spectral sequence and the degree of d is what we expect -/
+  definition convergence_0 (n : ℤ) (H : Πm, lb c m = 0) :
+    is_built_from (Dinf n) (λ(k : ℕ), Einf c (n - k, k)) :=
+  is_built_from_isomorphism isomorphism.rfl
+    (λk, left_module.isomorphism_of_eq (ap (Einf c)
+      (prod_eq (ap (sub n) (ap (add _) !H ⬝ add_zero _)) (ap (add _) !H ⬝ add_zero _))))
+    (HDinf c n)
+
+  /- we call a spectral sequence normal if it is a first-quadrant spectral sequence and
+    the degree of d on page r (for r ≥ 2) is (r, -(r-1)).
+    The indexing is different, because we start counting pages at 2. -/
   include c
   structure is_normal : Type :=
     (normal1 : Π{n} s, n < 0 → is_contr (E' n s))
@@ -166,10 +175,7 @@ namespace spectral_sequence
       refine lt_of_lt_of_le H2 (le.trans _ (le_of_eq !add_zero⁻¹)),
       exact add_le_add_right (of_nat_le_of_nat_of_le Hr') 1 },
   end
-  /- some properties which use the degree of the spectral sequence we construct. For the AHSS and SSS the hypothesis is by reflexivity -/
-
-
---  definition foo
+  omit d
 
 
 end spectral_sequence
diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index e58ccb1..ad25140 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -79,7 +79,7 @@ namespace group
 
   variables {G₁ G₂ : Group}
 
-  -- TODO: maybe define this in more generality for pointed propertys?
+  -- TODO: maybe define this in more generality for pointed sets?
   definition kernel [constructor] (φ : G₁ →g G₂) : property G₁ := { g | trunctype.mk (φ g = 1) _}
 
   theorem mul_mem_kernel (φ : G₁ →g G₂) (g h : G₁) (H₁ : g ∈ kernel φ) (H₂ : h ∈ kernel φ) : g * h ∈ kernel φ :=
@@ -555,6 +555,17 @@ end
     intro r, induction r, reflexivity
   end
 
+  definition is_equiv_incl_of_subgroup {G : Group} (H : property G) [is_subgroup G H]
+    (h : Πg, g ∈ H) : is_equiv (incl_of_subgroup H) :=
+  have is_surjective (incl_of_subgroup H),
+  begin intro g, exact image.mk ⟨g, h g⟩ idp end,
+  have is_embedding (incl_of_subgroup H), from is_embedding_incl_of_subgroup H,
+  function.is_equiv_of_is_surjective_of_is_embedding (incl_of_subgroup H)
+
+  definition subgroup_isomorphism [constructor] {G : Group} (H : property G) [is_subgroup G H]
+    (h : Πg, g ∈ H) : subgroup H ≃g G :=
+  isomorphism.mk _ (is_equiv_incl_of_subgroup H h)
+
 end group
 
 open group
diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean
index 0e2722e..6fdd463 100644
--- a/algebra/submodule.hlean
+++ b/algebra/submodule.hlean
@@ -5,41 +5,6 @@ import .left_module .quotient_group
 
 open algebra eq group sigma sigma.ops is_trunc function trunc equiv is_equiv property
 
-  definition group_homomorphism_of_add_group_homomorphism [constructor] {G₁ G₂ : AddGroup}
-    (φ : G₁ →a G₂) : G₁ →g G₂ :=
-  φ
-
--- move to subgroup
--- attribute normal_subgroup_rel._trans_of_to_subgroup_rel [unfold 2]
--- attribute normal_subgroup_rel.to_subgroup_rel [constructor]
-
-  definition is_equiv_incl_of_subgroup {G : Group} (H : property G) [is_subgroup G H] (h : Πg, g ∈ H) :
-    is_equiv (incl_of_subgroup H) :=
-  have is_surjective (incl_of_subgroup H),
-  begin intro g, exact image.mk ⟨g, h g⟩ idp end,
-  have is_embedding (incl_of_subgroup H), from is_embedding_incl_of_subgroup H,
-  function.is_equiv_of_is_surjective_of_is_embedding (incl_of_subgroup H)
-
-definition subgroup_isomorphism [constructor] {G : Group} (H : property G) [is_subgroup G H] (h : Πg, g ∈ H) :
-  subgroup H ≃g G :=
-isomorphism.mk _ (is_equiv_incl_of_subgroup H h)
-
-definition is_equiv_qg_map {G : Group} (H : property G) [is_normal_subgroup G H] (H₂ : Π⦃g⦄, g ∈ H → g = 1) :
-  is_equiv (qg_map H) :=
-set_quotient.is_equiv_class_of _ (λg h r, eq_of_mul_inv_eq_one (H₂ r))
-
-definition quotient_group_isomorphism [constructor] {G : Group} (H : property G) [is_normal_subgroup G H]
-  (h : Πg, g ∈ H → g = 1) : quotient_group H ≃g G :=
-(isomorphism.mk _ (is_equiv_qg_map H h))⁻¹ᵍ
-
-definition is_equiv_ab_qg_map {G : AbGroup} (H : property G) [is_subgroup G H] (h : Π⦃g⦄, g ∈ H → g = 1) :
-  is_equiv (ab_qg_map H) :=
-proof @is_equiv_qg_map G H (is_normal_subgroup_ab _) h qed
-
-definition ab_quotient_group_isomorphism [constructor] {G : AbGroup} (H : property G) [is_subgroup G H]
-  (h : Πg, H g → g = 1) : quotient_ab_group H ≃g G :=
-(isomorphism.mk _ (is_equiv_ab_qg_map H h))⁻¹ᵍ
-
 namespace left_module
 /- submodules -/
 variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R} {m m₁ m₂ : M}
@@ -61,7 +26,7 @@ transport (λx, S x) (by rewrite [add.comm, neg_add_cancel_left]) H
 
 -- open is_submodule
 
-variables {S : property M} [is_submodule M S]
+variables {S : property M} [is_submodule M S] {S₂ : property M₂} [is_submodule M₂ S₂]
 
 definition is_subgroup_of_is_submodule [instance] (S : property M) [is_submodule M S] :
   is_subgroup (AddGroup_of_AddAbGroup M) S :=
@@ -221,22 +186,29 @@ definition quotient_map [constructor] : M →lm quotient_module S :=
 lm_homomorphism_of_group_homomorphism (ab_qg_map _) (λr g, idp)
 
 definition quotient_map_eq_zero (m : M) (H : S m) : quotient_map S m = 0 :=
-@qg_map_eq_one _ _ (is_normal_subgroup_ab _) _ H
+@ab_qg_map_eq_one _ _ _ _ H
 
 definition rel_of_quotient_map_eq_zero (m : M) (H : quotient_map S m = 0) : S m :=
-@rel_of_qg_map_eq_one _ _ (is_normal_subgroup_ab _) m H
+@rel_of_qg_map_eq_one _ _ _ m H
 
 variable {S}
+definition respect_smul_quotient_elim [constructor] (φ : M →lm M₂) (H : Π⦃m⦄, m ∈ S → φ m = 0)
+  (r : R) (m : quotient_module S) :
+  quotient_ab_group_elim (group_homomorphism_of_lm_homomorphism φ) H
+    (@has_scalar.smul _ (quotient_module S) _ r m) =
+  r • quotient_ab_group_elim (group_homomorphism_of_lm_homomorphism φ) H m :=
+begin
+  revert m,
+  refine @set_quotient.rec_prop _ _ _ (λ x, !is_trunc_eq) _,
+  intro m,
+  exact to_respect_smul φ r m
+end
+
 definition quotient_elim [constructor] (φ : M →lm M₂) (H : Π⦃m⦄, m ∈ S → φ m = 0) :
   quotient_module S →lm M₂ :=
 lm_homomorphism_of_group_homomorphism
   (quotient_ab_group_elim (group_homomorphism_of_lm_homomorphism φ) H)
-  begin
-    intro r, esimp,
-    refine @set_quotient.rec_prop _ _ _ (λ x, !is_trunc_eq) _,
-    intro m,
-    exact to_respect_smul φ r m
-  end
+  (respect_smul_quotient_elim φ H)
 
 definition is_prop_quotient_module (S : property M) [is_submodule M S] [H : is_prop M] : is_prop (quotient_module S) :=
 begin apply @set_quotient.is_trunc_set_quotient, exact H end
@@ -255,6 +227,17 @@ definition quotient_module_isomorphism [constructor] (S : property M) [is_submod
   quotient_module S ≃lm M :=
 (isomorphism.mk (quotient_map S) (is_equiv_ab_qg_map S h))⁻¹ˡᵐ
 
+definition quotient_module_functor [constructor] (φ : M →lm M₂) (h : Πg, g ∈ S → φ g ∈ S₂) :
+  quotient_module S →lm quotient_module S₂ :=
+quotient_elim (quotient_map S₂ ∘lm φ)
+  begin intros m Hm, rexact quotient_map_eq_zero S₂ (φ m) (h m Hm) end
+
+definition quotient_module_isomorphism_quotient_module [constructor] (φ : M ≃lm M₂)
+    (h : Πm, m ∈ S ↔ φ m ∈ S₂) : quotient_module S ≃lm quotient_module S₂ :=
+lm_isomorphism_of_group_isomorphism
+  (quotient_ab_group_isomorphism_quotient_ab_group (group_isomorphism_of_lm_isomorphism φ) h)
+  (to_respect_smul (quotient_module_functor φ (λg, iff.mp (h g))))
+
 /- specific submodules -/
 definition has_scalar_image (φ : M₁ →lm M₂) ⦃m : M₂⦄ (r : R)
   (h : image φ m) : image φ (r • m) :=
@@ -455,6 +438,57 @@ definition is_surjective_of_is_contr_homology_of_is_contr (ψ : M₂ →lm M₃)
   (H₁ : is_contr (homology ψ φ)) (H₂ : is_contr M₃) : is_surjective φ :=
 is_surjective_of_is_contr_homology_of_constant ψ H₁ (λm, @eq_of_is_contr _ H₂ _ _)
 
+definition cokernel_module (φ : M₁ →lm M₂) : LeftModule R :=
+quotient_module (image φ)
+
+definition cokernel_module_isomorphism_homology (φ : M₁ →lm M₂) :
+  homology (trivial_homomorphism M₂ (trivial_LeftModule R)) φ ≃lm cokernel_module φ :=
+quotient_module_isomorphism_quotient_module
+  (submodule_isomorphism _ (λm, idp))
+  begin intro m, reflexivity end
+
+open chain_complex fin nat
+definition LES_of_SESs.{u} {N : succ_str} (A B C : N → LeftModule.{_ u} R) (φ : Πn, A n →lm B n)
+  (ses : Πn : N, short_exact_mod (cokernel_module (φ (succ_str.S n))) (C n) (kernel_module (φ n))) :
+  chain_complex.{_ u} (stratified N 2) :=
+begin
+  fapply chain_complex.mk,
+  { intro x, apply @pSet_of_LeftModule R,
+    induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1),
+    { /-k≥3-/ exfalso, apply lt_le_antisymm H, apply le_add_left},
+    { /-k=0-/ exact B n },
+    { /-k=1-/ exact A n },
+    { /-k=2-/ exact C n }},
+  { intro x, apply @pmap_of_homomorphism R,
+    induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1),
+    { /-k≥3-/ exfalso, apply lt_le_antisymm H, apply le_add_left},
+    { /-k=0-/ exact φ n },
+    { /-k=1-/ exact submodule_incl _ ∘lm short_exact_mod.g (ses n) },
+    { /-k=2-/ change B (succ_str.S n) →lm C n, exact short_exact_mod.f (ses n) ∘lm !quotient_map }},
+  { intros x m, induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1),
+    { exfalso, apply lt_le_antisymm H, apply le_add_left},
+    { exact (short_exact_mod.g (ses n) m).2 },
+    { exact ap pr1 (is_short_exact.im_in_ker (short_exact_mod.h (ses n)) (quotient_map _ m)) },
+    { exact ap (short_exact_mod.f (ses n)) (quotient_map_eq_zero _ _ (image.mk m idp)) ⬝
+            to_respect_zero (short_exact_mod.f (ses n)) }}
+end
+
+definition is_exact_LES_of_SESs.{u} {N : succ_str} (A B C : N → LeftModule.{_ u} R) (φ : Πn, A n →lm B n)
+  (ses : Πn : N, short_exact_mod (cokernel_module (φ (succ_str.S n))) (C n) (kernel_module (φ n))) :
+  is_exact (LES_of_SESs A B C φ ses) :=
+begin
+  intros x m p, induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1),
+  { exfalso, apply lt_le_antisymm H, apply le_add_left},
+  { induction is_short_exact.is_surj (short_exact_mod.h (ses n)) ⟨m, p⟩ with m' q,
+    exact image.mk m' (ap pr1 q) },
+  { induction is_short_exact.ker_in_im (short_exact_mod.h (ses n)) m (subtype_eq p) with m' q,
+    induction m' using set_quotient.rec_prop with m',
+    exact image.mk m' q },
+  { apply rel_of_quotient_map_eq_zero (image (φ (succ_str.S n))) m,
+    apply @is_injective_of_is_embedding _ _ _ (is_short_exact.is_emb (short_exact_mod.h (ses n))),
+    exact p ⬝ (to_respect_zero (short_exact_mod.f (ses n)))⁻¹ }
+end
+
 -- remove:
 
 -- definition homology.rec (P : homology ψ φ → Type)
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 381cc5f..83e5c09 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -157,6 +157,10 @@ end sigma open sigma
 
 namespace group
 
+  definition group_homomorphism_of_add_group_homomorphism [constructor] {G₁ G₂ : AddGroup}
+    (φ : G₁ →a G₂) : G₁ →g G₂ :=
+  φ
+
 
 --  definition is_equiv_isomorphism