From 6de6e72a035dc403bcdfed1ace0f16b24f5fcdfd Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Tue, 23 Jan 2018 12:44:01 -0500
Subject: [PATCH] simplify proof of is_trunc_Grp

---
 higher_groups.hlean | 9 ++-------
 move_to_lib.hlean   | 7 +++++++
 2 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/higher_groups.hlean b/higher_groups.hlean
index 4765edf..79a8a9d 100644
--- a/higher_groups.hlean
+++ b/higher_groups.hlean
@@ -247,13 +247,8 @@ begin
   apply @is_trunc_equiv_closed_rev _ _ _ (ptruncconntype_eq_equiv X Y),
   apply @is_trunc_equiv_closed_rev _ _ _ (pequiv.sigma_char_equiv' X Y),
   apply @is_trunc_subtype (X →* Y) (λ f, trunctype.mk' -1 (is_equiv f)),
-  apply is_trunc_pmap_of_is_conn X k.-2 (n + 1).-2 (n + k) Y,
-  { clear X Y, induction k with k IH,
-    { induction n with n IH,
-      { apply le.refl },
-      { exact trunc_index.succ_le_succ IH } },
-    { rewrite (trunc_index.succ_add_plus_two (nat.succ k).-2 (n + 1).-2),
-      exact trunc_index.succ_le_succ IH } },
+  apply is_trunc_pmap_of_is_conn X k.-2 (n.-1) (n + k) Y,
+  { apply le_of_eq, exact (sub_one_add_plus_two_sub_one n k)⁻¹ ⬝ !add_plus_two_comm },
   { exact _ }
 end
 
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 3e0b04e..671a14f 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -424,6 +424,13 @@ namespace trunc_index
     { exact !succ_add_plus_two ⬝ ap succ IH}
   end
 
+  lemma sub_one_add_plus_two_sub_one (n m : ℕ) : n.-1 +2+ m.-1 = of_nat (n + m) :=
+  begin
+    induction m with m IH,
+    { reflexivity },
+    { exact ap succ IH }
+  end
+
 end trunc_index
 
 namespace int