diff --git a/thue-morse.v b/thue-morse.v
index 79200e7..d4603a8 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1302,9 +1302,10 @@ Proof.
    rewrite M. apply tm_morphism_size.
 
    assert (2 <= length (b++b++b++tl2)).
-   rewrite app_length. replace (2) with (2+0). apply Nat.add_le_mono. assumption.
-   apply Nat.le_0_l. apply Nat.add_0_r.
-   rewrite H3 in H4. replace (2) with (2*1) in H4. rewrite <- Nat.mul_le_mono_pos_l in H4.
+   rewrite app_length. rewrite <- Nat.add_0_r at 1.
+   apply Nat.add_le_mono. assumption. apply Nat.le_0_l.
+   rewrite H3 in H4. rewrite <- Nat.mul_1_r in H4 at 1.
+   rewrite <- Nat.mul_le_mono_pos_l in H4.
     
    rewrite firstn_length. rewrite <- Nat.le_succ_l.
    assert (1 <= Nat.div2 (length b)).
@@ -1314,7 +1315,7 @@ Proof.
    rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r. reflexivity.
    apply Nat.lt_0_2.
    generalize H4. generalize H5. apply Nat.min_glb.
-   apply Nat.lt_0_2. easy.
+   apply Nat.lt_0_2.
 Qed.