diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean
index 5240c7d..6132e96 100644
--- a/algebra/spectral_sequence.hlean
+++ b/algebra/spectral_sequence.hlean
@@ -845,18 +845,18 @@ namespace spectrum
                   ij_sequence jk_sequence ki_sequence
 
   open int
-  parameters (ub : ℤ) (lb : ℤ → ℤ)
-    (Aub : Π(s n : ℤ), s ≥ ub + 1 → is_equiv (f s n))
+  parameters (ub : ℤ → ℤ) (lb : ℤ → ℤ)
+    (Aub : Π(s n : ℤ), s ≥ ub n + 1 → is_equiv (πₛ→[n] (f s)))
     (Alb : Π(s n : ℤ), s ≤ lb n → is_contr (πₛ[n] (A s)))
 
   definition B : I → ℕ
   | (n, s) := max0 (s - lb n)
 
   definition B' : I → ℕ
-  | (n, s) := max0 (ub - s)
+  | (n, s) := max0 (ub n - s)
 
   definition B'' : I → ℕ
-  | (n, s) := max0 (ub + 1 - s)
+  | (n, s) := max0 (max (ub n + 1 - s) (ub (n+1) + 1 - s))
 
   lemma iterate_deg_i (n s : ℤ) (m : ℕ) : (deg i_sequence)^[m] (n, s) = (n, s - m) :=
   begin
@@ -884,7 +884,6 @@ namespace spectrum
     is_surjective (i_sequence ((deg i_sequence)⁻¹ᵉ^[t+1] x)) :=
   begin
     apply is_surjective_of_is_equiv,
-    apply is_equiv_homotopy_group_functor,
     apply Aub, induction x with n s,
     rewrite [iterate_deg_i_inv, ▸*, of_nat_add, -add.assoc],
     apply add_le_add_right,
@@ -894,12 +893,13 @@ namespace spectrum
 
   lemma Elb ⦃x : I⦄ ⦃t : ℕ⦄ (h : B'' x ≤ t) : is_contr (E_sequence ((deg i_sequence)⁻¹ᵉ^[t] x)) :=
   begin
-    apply is_contr_homotopy_group_of_is_contr,
-    apply is_contr_fiber_of_is_equiv,
-    apply Aub, induction x with n s,
+    induction x with n s,
     rewrite [iterate_deg_i_inv, ▸*],
-    apply le_add_of_sub_left_le,
-    apply le_of_max0_le h,
+    apply is_contr_shomotopy_group_sfiber_of_is_equiv,
+    apply Aub, apply le_add_of_sub_left_le, apply le_of_max0_le, refine le.trans _ h,
+    apply max0_monotone, apply le_max_left,
+    apply Aub, apply le_add_of_sub_left_le, apply le_of_max0_le, refine le.trans _ h,
+    apply max0_monotone, apply le_max_right
   end
 
   definition is_bounded_sequence [constructor] : is_bounded exact_couple_sequence :=
@@ -910,13 +910,13 @@ namespace spectrum
       refine !add.assoc ⬝ ap (add s) !add.comm ⬝ !add.assoc⁻¹,
     end
 
-  definition converges_to_sequence : (λn s, πₛ[n] (sfiber (f s))) ⟹ᵍ (λn, πₛ[n] (A ub)) :=
+  definition converges_to_sequence : (λn s, πₛ[n] (sfiber (f s))) ⟹ᵍ (λn, πₛ[n] (A (ub n))) :=
   begin
     fapply converges_to.mk,
     { exact exact_couple_sequence },
     { exact is_bounded_sequence },
-    { intro n, exact ub },
-    { intro n, change max0 (ub - ub) = 0, exact ap max0 (sub_self ub) },
+    { exact ub },
+    { intro n, change max0 (ub n - ub n) = 0, exact ap max0 (sub_self (ub n)) },
     { intro ns, reflexivity },
     { intro n, reflexivity },
     { intro r, exact - 1 },
diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean
index e84db26..e7b66e5 100644
--- a/cohomology/serre.hlean
+++ b/cohomology/serre.hlean
@@ -128,12 +128,13 @@ qed
 
 section atiyah_hirzebruch
   parameters {X : Type*} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x))
+  include H
 
   definition atiyah_hirzebruch_exact_couple : exact_couple rℤ Z2 :=
   @exact_couple_sequence (λs, spi X (λx, strunc s (Y x)))
                          (λs, spi_compose_left (λx, postnikov_smap (Y x) s))
 
-  include H
+--  include H
   definition atiyah_hirzebruch_ub ⦃s n : ℤ⦄ (Hs : s ≤ n - 1) :
     is_contr (πₛ[n] (spi X (λx, strunc s (Y x)))) :=
   begin
@@ -141,7 +142,7 @@ section atiyah_hirzebruch
     apply is_strunc_spi, intro x, exact is_strunc_strunc _ _
   end
 
-  definition atiyah_hirzebruch_lb ⦃s n : ℤ⦄ (Hs : s ≥ s₀ + 1) :
+  definition atiyah_hirzebruch_lb' ⦃s n : ℤ⦄ (Hs : s ≥ s₀ + 1) :
     is_equiv (spi_compose_left (λx, postnikov_smap (Y x) s) n) :=
   begin
     refine is_equiv_of_equiv_of_homotopy
@@ -161,13 +162,19 @@ section atiyah_hirzebruch
     reflexivity
   end
 
+  definition atiyah_hirzebruch_lb ⦃s n : ℤ⦄ (Hs : s ≥ s₀ + 1) :
+    is_equiv (πₛ→[n] (spi_compose_left (λx, postnikov_smap (Y x) s))) :=
+  begin
+    apply is_equiv_homotopy_group_functor, apply atiyah_hirzebruch_lb', exact Hs
+  end
+
   definition is_bounded_atiyah_hirzebruch : is_bounded atiyah_hirzebruch_exact_couple :=
-  is_bounded_sequence _ s₀ (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub
+  is_bounded_sequence _ (λn, s₀) (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub
 
   definition atiyah_hirzebruch_convergence' :
     (λn s, πₛ[n] (sfiber (spi_compose_left (λx, postnikov_smap (Y x) s)))) ⟹ᵍ
     (λn, πₛ[n] (spi X (λx, strunc s₀ (Y x)))) :=
-  converges_to_sequence _ s₀ (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub
+  converges_to_sequence _ (λn, s₀) (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub
 
   definition atiyah_hirzebruch_convergence :
     (λn s, opH^-(n-s)[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, pH^-n[(x : X), Y x]) :=
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index b06fc71..37ead01 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -59,6 +59,16 @@ namespace nat
 
 end nat
 
+  definition max0_monotone {n m : ℤ} (H : n ≤ m) : max0 n ≤ max0 m :=
+  begin
+    induction n with n n,
+    { induction m with m m,
+      { exact le_of_of_nat_le_of_nat H },
+      { exfalso, exact not_neg_succ_le_of_nat H }},
+    { apply zero_le }
+  end
+
+
   -- definition ppi_eq_equiv_internal : (k = l) ≃ (k ~* l) :=
   --   calc (k = l) ≃ ppi.sigma_char P p₀ k = ppi.sigma_char P p₀ l
   --                  : eq_equiv_fn_eq (ppi.sigma_char P p₀) k l
@@ -1494,3 +1504,18 @@ namespace category
   isomorphism.mk _ (is_isomorphism_pb_Precategory_functor C f)
 
 end category
+
+namespace chain_complex
+  open fin
+  definition is_contr_homotopy_group_fiber {A B : pType.{u}} {f : A →* B} {n : ℕ}
+    (H1 : is_embedding (π→[n] f)) (H2 : is_surjective (π→g[n+1] f)) : is_contr (π[n] (pfiber f)) :=
+  begin
+    apply @is_contr_of_is_embedding_of_is_surjective +3ℕ (LES_of_homotopy_groups f) (n, 0),
+    exact is_exact_LES_of_homotopy_groups f (n, 1), exact H1, exact H2
+  end
+
+  definition is_contr_homotopy_group_fiber_of_is_equiv {A B : pType.{u}} {f : A →* B} {n : ℕ}
+    (H1 : is_equiv (π→[n] f)) (H2 : is_equiv (π→g[n+1] f)) : is_contr (π[n] (pfiber f)) :=
+  is_contr_homotopy_group_fiber (is_embedding_of_is_equiv _) (is_surjective_of_is_equiv _)
+
+end chain_complex
diff --git a/pointed_pi.hlean b/pointed_pi.hlean
index eb3cfdd..ca97908 100644
--- a/pointed_pi.hlean
+++ b/pointed_pi.hlean
@@ -846,6 +846,22 @@ namespace pointed
     { exact !ppi_eq_equiv_natural_gen_refl ◾ (!idp_con ⬝ !eq_of_phomotopy_refl) }
   end
 
+  definition loopn_pppi_pequiv [constructor] (n : ℕ) {A : Type*} (B : A → Type*) :
+    Ω[n] (Π*a, B a) ≃* Π*(a : A), Ω[n] (B a) :=
+  begin
+    induction n with n IH,
+    { reflexivity },
+    { refine loop_pequiv_loop IH ⬝e* loop_pppi_pequiv (λa, Ω[n] (B a)) }
+  end
+
+  -- definition trivial_homotopy_group_pppi {A : Type*} {B : A → Type*} {n : ℕ}
+  --   (H : Πa, is_contr (Ω[n] (B a))) : is_contr (π[n] (Π*a, B a)) :=
+  -- begin
+  --   apply is_trunc_trunc_of_is_trunc,
+  --   apply is_trunc_equiv_closed_rev,
+  --   apply loopn_pppi_pequiv
+  -- end
+
 
 /- below is an alternate proof strategy for the naturality of loop_pppi_pequiv_natural,
   where we define loop_pppi_pequiv as composite of pointed equivalences, and proved the
diff --git a/spectrum/basic.hlean b/spectrum/basic.hlean
index 54815fb..da21edb 100644
--- a/spectrum/basic.hlean
+++ b/spectrum/basic.hlean
@@ -703,8 +703,25 @@ namespace spectrum
                              πg_glue Y n ∘g (by reflexivity) qed
   | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
 --(homomorphism_LES_of_homotopy_groups_fun (f (2 - n)) (1, 2) ∘g πg_glue Y n)
+
+  definition is_contr_shomotopy_group_sfiber {n : ℤ}
+    (H1 : is_embedding (πₛ→[n] f)) (H2 : is_surjective (πₛ→[n+1] f)) :
+    is_contr (πₛ[n] (sfiber f)) :=
+  begin
+    apply @is_contr_of_is_embedding_of_is_surjective +3ℤ LES_of_shomotopy_groups (n, 0),
+    exact is_exact_LES_of_shomotopy_groups (n, 1), exact H1, exact H2
+  end
+
+  definition is_contr_shomotopy_group_sfiber_of_is_equiv {n : ℤ}
+    (H1 : is_equiv (πₛ→[n] f)) (H2 : is_equiv (πₛ→[n+1] f)) :
+    is_contr (πₛ[n] (sfiber f)) :=
+  proof
+    is_contr_shomotopy_group_sfiber (is_embedding_of_is_equiv _) (is_surjective_of_is_equiv _)
+  qed
+
   end LES
 
+
   /- homotopy group of a prespectrum -/
 
   definition pshomotopy_group_hom (n : ℤ) (E : prespectrum) (k : ℕ)