From c111795caa226be197b70cb196506fad8d118b2f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Jan 2021 18:53:43 +0100
Subject: [PATCH] simplify proof (by Robbert)

---
 theories/list_numbers.v | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 1caa8ede..c3365b65 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -145,15 +145,9 @@ Section seqZ.
     0 ≤ n2 →
     seqZ m (n1 + n2) = seqZ m n1 ++ seqZ (m + n1) n2.
   Proof.
-    intros. unfold seqZ.
-    replace (Z.to_nat (n1 + n2)) with (Z.to_nat n1 + Z.to_nat n2)%nat by lia.
-    rewrite seq_app, fmap_app.
-    f_equal.
-    replace (0 + Z.to_nat n1)%nat with (Z.to_nat n1 + 0)%nat by lia.
-    rewrite <- fmap_add_seq.
-    rewrite <- list_fmap_compose.
-    apply list_fmap_ext; auto.
-    intros. simpl. lia.
+    intros. unfold seqZ. rewrite Z2Nat.inj_add, seq_app, fmap_app by done.
+    f_equal. rewrite Nat.add_comm, <-!fmap_add_seq, <-list_fmap_compose.
+    apply list_fmap_ext; naive_solver auto with lia.
   Qed.
 
   Lemma seqZ_S m i : seqZ m (S i) = seqZ m i ++ [m + i].
-- 
GitLab