Update

thue-morse.v

@@ -1117,6 +1117,47 @@ Proof.
     + simpl in H. symmetry in H. apply Bool.diff_true_false in H. contradiction H.
 Qed.
 
+
+Lemma lt_split_bits : forall n m k j,
+  0 < k -> j < 2^m -> k*2^m < 2^n -> k*2^m+j < 2^n.
+Proof.
+  intros n m k j. intros H I J.
+
+  assert (K: 2^m <= k*2^m). rewrite <- Nat.mul_1_l at 1.
+  apply Nat.mul_le_mono_r. rewrite Nat.le_succ_l. assumption.
+
+  assert (L:2^m < 2^n). generalize J. generalize K. apply Nat.le_lt_trans.
+
+  assert (k < 2^(n-m)). rewrite Nat.mul_lt_mono_pos_r with (p := 2^m).
+  rewrite <- Nat.pow_add_r. rewrite Nat.sub_add. assumption.
+  apply Nat.pow_lt_mono_r_iff in L. apply Nat.lt_le_incl. assumption.
+  apply Nat.lt_1_2. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+
+  replace (2^(n-m)) with (S (2^(n-m)-1)) in H0. rewrite Nat.lt_succ_r in H0.
+  apply Nat.mul_le_mono_r with (p := 2^m) in H0.
+  rewrite Nat.mul_sub_distr_r in H0. rewrite Nat.mul_1_l in H0.
+  rewrite <- Nat.pow_add_r in H0. rewrite Nat.sub_add in H0.
+
+  rewrite Nat.add_le_mono_r with (p := j) in H0.
+  assert (2^n - 2^m + j < 2^n).
+  rewrite Nat.add_lt_mono_l with (p := 2^n) in I.
+  rewrite Nat.add_lt_mono_r with (p := 2^m).
+  rewrite <- Nat.add_assoc. rewrite <- Nat.add_sub_swap.
+  rewrite Nat.add_assoc. rewrite Nat.add_sub. assumption.
+
+  apply Nat.lt_le_incl. assumption.
+  generalize H1. generalize H0. apply Nat.le_lt_trans.
+  apply Nat.lt_le_incl. rewrite <- Nat.pow_lt_mono_r_iff in L. assumption.
+  apply Nat.lt_1_2. rewrite <- Nat.add_1_r. apply Nat.sub_add.
+  rewrite Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+Qed.
+
+
+
+  (* TODO: supprimer lt_even_even après avoir réussi ce truc ??? *)
+
+
+
 Lemma lt_split_bits : forall n m k j,
   0 < k -> j < m -> k * 2^m < 2^n -> k * 2^m +2^j < 2^n.
 Proof.
@@ -1173,6 +1214,8 @@ Proof.
 Qed.
 
 (* TODO: truc suivant inutile ? *)
+(* TODO: réécrire en plus puissant avec i et j < 2^m et on ajoute
+  désormais direcctement i et j au lieu d'ajouter 2^i et 2^j *)
 Lemma tm_step_repeating_patterns :
   forall (n m i j : nat),
   i < m -> j < m