diff --git a/thue-morse.v b/thue-morse.v index bc6ccc6..d82db4a 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -746,7 +746,6 @@ Proof. apply Nat.lt_trans. rewrite tm_size_power2. assumption. - rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_1_r. rewrite <- Nat.sub_succ_l. rewrite Nat.sub_succ. reflexivity.