diff --git a/src/thue_morse2.v b/src/thue_morse2.v index d620783..bcae771 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -1063,7 +1063,6 @@ Proof. Qed. - Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> 0 < length a @@ -1465,10 +1464,3 @@ Proof. rewrite <- Nat.negb_odd. rewrite <- Nat.negb_odd. rewrite H0. rewrite H1. reflexivity. Qed. - - - (* TODO: la taille du facteur divise la taille du préfixe ? *) - (* TODO : le cas de la taille 2 est un cas pair facile - grâce à tm_step_factor4_odd_prefix *) - - (* TODO: revoir tm_step_cube4 *)