utils: simplification of proofs

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>

src/utils.v

@@ -9,9 +9,7 @@ Proof.
   induction l.
   - reflexivity.
   - simpl.
-    destruct f.
-    + discriminate.
-    + exact IHl.
+    now destruct f.
 Qed.
 
 Lemma nth_error_on_composed_list :
@@ -26,8 +24,7 @@ Proof.
     simpl.
     lia.
 
-  - rewrite (nth_error_nth' _ d Hlength), Hl, Hi, nth_middle.
-    reflexivity.
+  - now rewrite (nth_error_nth' _ d Hlength), Hl, Hi, nth_middle.
 Qed.
 
 Lemma map_in_the_middle :
@@ -36,13 +33,7 @@ Lemma map_in_the_middle :
     List.nth_error (List.map f l) i = Some (f a).
 Proof.
   intros A B a d f l lpre lpost i Hl Hi.
-
-  assert (List.nth_error l i = Some a) as Hnth.
-  apply (nth_error_on_composed_list _ _ d _ lpre lpost);
-    assumption.
-
-  rewrite (map_nth_error _ i l Hnth).
-  reflexivity.
+  now apply map_nth_error, (nth_error_on_composed_list _ _ d _ lpre lpost).
 Qed.
 
 Section ListCustomBool.