diff --git a/src/thue_morse.v b/src/thue_morse.v
index 29f1bcc..65718b8 100644
--- a/src/thue_morse.v
+++ b/src/thue_morse.v
@@ -347,19 +347,18 @@ Proof.
   destruct k.
   - rewrite Nat.mul_0_r. rewrite tm_step_head_1. simpl.
     rewrite tm_step_head_1. reflexivity.
-  - rewrite <- tm_step_lemma.
-    rewrite tm_morphism_double_index. reflexivity.
+  - rewrite <- tm_step_lemma. apply tm_morphism_double_index.
 Qed.
 
 Lemma tm_step_single_bit_index : forall (n : nat),
   nth_error (tm_step (S n)) (2^n) = Some true.
 Proof.
   intro n.
-  rewrite tm_build. rewrite nth_error_app2.
-  - rewrite tm_size_power2. rewrite Nat.sub_diag.
+  rewrite tm_build. rewrite nth_error_app2; rewrite tm_size_power2.
+  - rewrite Nat.sub_diag.
     replace (true) with (negb false). apply map_nth_error.
     rewrite tm_step_head_1. reflexivity. reflexivity.
-  - rewrite tm_size_power2. apply Nat.le_refl.
+  - apply Nat.le_refl.
 Qed.
 
 Lemma tm_step_repunit_index : forall (n : nat),
@@ -414,7 +413,7 @@ Lemma tm_step_add_range : forall (n m k : nat),
 Proof.
   intros n m k. intro H.
   induction m.
-  - rewrite Nat.add_comm. reflexivity.
+  - rewrite Nat.add_0_r. reflexivity.
   - rewrite Nat.add_succ_r. rewrite <- tm_size_power2 in H.
     assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
     generalize H. apply nth_error_nth'.
@@ -434,15 +433,13 @@ Proof.
     apply Nat.add_sub_assoc. rewrite Nat.add_comm.
     assert (n <= n). apply le_n. symmetry.
     replace (m) with (m + (n-n)) at 1. generalize H3.
-    apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
-    reflexivity.
+    apply Nat.add_sub_assoc. rewrite Nat.sub_diag. apply Nat.add_0_r.
   - destruct H1. symmetry. replace (n) with (m + (n - m)). apply tm_step_add_range.
     apply H0. replace (n) with (m + n - m) at 2. generalize H1.
     apply Nat.add_sub_assoc. rewrite Nat.add_comm.
     assert (m <= m). apply le_n. symmetry.
     replace (n) with (n + (m-m)) at 1. generalize H3.
-    apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
-    reflexivity.
+    apply Nat.add_sub_assoc. rewrite Nat.sub_diag. apply Nat.add_0_r.
 Qed.
 
 (**
@@ -512,11 +509,11 @@ Proof.
 
       rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
       rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
-      rewrite Nat.add_comm. reflexivity. assumption.
+      apply Nat.add_comm. assumption.
 
       rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
       rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
-      rewrite Nat.add_comm. reflexivity. assumption.
+      apply Nat.add_comm. assumption.
 
       rewrite tm_size_power2.
       assert (k*2^m <= k*2^m + j). apply Nat.le_add_r.
@@ -709,7 +706,7 @@ Proof.
 
   assert (N: nth_error (tm_step m) (2^j) = Some true).
   replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)).
-  rewrite tm_step_single_bit_index. reflexivity.
+  apply tm_step_single_bit_index.
   apply tm_step_stable.
   apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_succ_diag_r.
   assumption.
@@ -948,7 +945,7 @@ Proof.
     rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3.
     assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l.
     rewrite app_assoc_reverse. rewrite app_inv_head_iff.
-    rewrite app_assoc_reverse. reflexivity.
+    apply app_assoc_reverse.
 
     assert (I := H). replace (hd++a++a++a++tl) with ((hd++a)++(a++a++tl)) in I.
     assert (count_occ Bool.bool_dec (hd++a) true = count_occ Bool.bool_dec (hd++a) false).
@@ -978,11 +975,11 @@ Proof.
     rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3.
     rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3.
     assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l.
-    rewrite app_assoc_reverse. reflexivity.
+    apply app_assoc_reverse.
     rewrite app_assoc_reverse. rewrite app_inv_head_iff.
     rewrite app_assoc_reverse. rewrite app_inv_head_iff.
-    rewrite app_assoc_reverse. reflexivity.
-    rewrite app_assoc_reverse. rewrite app_inv_head_iff. reflexivity.
+    apply app_assoc_reverse.
+    apply app_assoc_reverse.
 Qed.
 
 
@@ -1262,7 +1259,7 @@ Proof.
     generalize H0. symmetry in M. generalize M.
     replace (b++b++b++tl2) with ((b++b++b)++tl2). apply tm_morphism_app3.
     rewrite app_assoc_reverse. apply app_inv_head_iff.
-    rewrite app_assoc_reverse. reflexivity.
+    apply app_assoc_reverse.
     assert (hd2 ++ b ++ b ++ b ++ tl2
       = (tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n)))
       ++ (tm_morphism (firstn (Nat.div2 (length b))