diff --git a/thue-morse.v b/thue-morse.v index 10b31c2..6060bb1 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1110,7 +1110,10 @@ Lemma tm_step_next_range2_neighbor' : forall (n k : nat), rewrite <- H2. rewrite <- H3. apply L. apply H0. - - + - induction m. + + intros L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L. + apply tm_step_next_range2_neighbor'. apply H. apply L. + +