diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 3235368..2333974 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -507,19 +507,16 @@ Proof.
   (* un sous-cas
                 (T F) | F T T F || F T T F | (F T)  cube
   *)
-  assert (b4 = b). destruct b4; destruct b1; destruct b.
-  reflexivity. contradiction n3. reflexivity. reflexivity.
-  contradiction n1. reflexivity. contradiction n1. reflexivity.
-  reflexivity. contradiction n3. reflexivity. reflexivity. rewrite H1 in H.
+  assert (b4 = b). destruct b4; destruct b1; destruct b;
+  reflexivity || contradiction n3 || contradiction n1; reflexivity.
+  rewrite H1 in H.
   assert (b2 = b). destruct b2; destruct b1; destruct b.
   reflexivity. contradiction n0. reflexivity. reflexivity.
   contradiction n1. reflexivity. contradiction n1. reflexivity.
   reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H2 in H.
   assert (last (b3::hd) false = b).
-  destruct (last (b3::hd) false); destruct b1; destruct b.
-  reflexivity. contradiction n2. reflexivity. reflexivity.
-  contradiction n1. reflexivity. contradiction n1. reflexivity.
-  reflexivity. contradiction n2. reflexivity. reflexivity.
+  destruct (last (b3::hd) false); destruct b1; destruct b;
+  reflexivity || contradiction n2 || contradiction n1; reflexivity.
 
        (* élargir hd et tl à l'aide des booléens b5 (gauche) et b6 (droite) *)
   destruct hd. inversion Q. destruct tl.
@@ -562,10 +559,9 @@ Proof.
       ++ [b] ++ [b] ++ [b] ++ tl) in H.
   apply tm_step_cubefree in H. contradiction H. reflexivity.
   apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
-  assert (b6 = b1). destruct (b6); destruct b1; destruct b.
-  reflexivity. reflexivity. contradiction n5. reflexivity.
-  contradiction n1. reflexivity. contradiction n1. reflexivity.
-  contradiction n5. reflexivity. reflexivity. reflexivity. rewrite H5 in H.
+  assert (b6 = b1). destruct (b6); destruct b1; destruct b;
+  reflexivity || contradiction n5 || contradiction n1; reflexivity.
+  rewrite H5 in H.
 
   (* contradiction *)
   replace (
@@ -642,10 +638,8 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
   destruct M. left. assumption. (* ici on postule le modulo = 2 *)
 
   assert (last (b3::hd) false = b1).
-  destruct (last (b3::hd) false); destruct b1; destruct b0.
-  reflexivity. reflexivity. contradiction n2. reflexivity.
-  contradiction n1. reflexivity. contradiction n1. reflexivity.
-  contradiction n2. reflexivity. reflexivity. reflexivity.
+  destruct (last (b3::hd) false); destruct b1; destruct b0;
+  reflexivity || contradiction n2 || contradiction n1; reflexivity.
 
   assert ({b4=b0} + {~ b4=b0}). apply bool_dec. destruct H3. rewrite e0 in H.
   assert (exists x, skipn 2 [b1;b0;b1;b0] = [x;x]).
@@ -664,10 +658,8 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
   destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
   contradiction n1. reflexivity.
 
-  assert (b4 = b1). destruct b4; destruct b1; destruct b0.
-  reflexivity. reflexivity. contradiction n3. reflexivity.
-  contradiction n1. reflexivity. contradiction n1. reflexivity.
-  contradiction n3. reflexivity. reflexivity. reflexivity.
+  assert (b4 = b1). destruct b4; destruct b1; destruct b0;
+  reflexivity || contradiction n3 || contradiction n1; reflexivity.
   rewrite H3 in H. rewrite H2 in H.
 
   assert (b2 = b0). destruct b2; destruct b1; destruct b0.
@@ -751,17 +743,13 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   rewrite <- app_assoc. reflexivity.
 
   (* on assigne les valeurs correctes aux deux extrémités *)
-  assert (b6 = b0). destruct b6; destruct b1; destruct b0.
-  reflexivity. contradiction n5. reflexivity. reflexivity.
-  contradiction n1. reflexivity. contradiction n1. reflexivity.
-  reflexivity. contradiction n5. reflexivity. reflexivity.
+  assert (b6 = b0). destruct b6; destruct b1; destruct b0;
+  reflexivity || contradiction n5 || contradiction n1; reflexivity.
   rewrite H5 in H.
   assert (last (removelast (b3 :: b5 :: hd)) false = b0).
   destruct (last (removelast (b3 :: b5 :: hd)) false);
-  destruct b1; destruct b0.
-  reflexivity. contradiction n4. reflexivity. reflexivity.
-  contradiction n1. reflexivity. contradiction n1. reflexivity.
-  reflexivity. contradiction n4. reflexivity. reflexivity.
+  destruct b1; destruct b0;
+  reflexivity || contradiction n4 || contradiction n1; reflexivity.
   rewrite H6 in H.
 
   (* on étend hd *)