proposition: Lemma nth_extend_middle {A} (a : A) n (l l' l'' : list A) : match Nat.compare n (length l') with | Lt => nth n (l' @ l) a = nth n (l' @ l'' @ l) a | _ => nth n (l' @ l) a = nth (n + length l'') (l' @ l'' @ l) a end.
proof: Proof. assert (foo:=Nat.compare_spec n (length l')). depelim foo; fold (length l') in H; try rewrite H0; try rewrite H. rewrite <- nth_extend_left. replace (length l'') with (length l'' + 0) by auto with arith. rewrite <- nth_extend_left. replace (length l') with (length l' + 0) by auto with arith. now rewrite <- nth_extend_left. clear H0. now rewrite !nth_app_l by trivial. clear H0. rewrite !nth_app_r by lia. f_equal. lia. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia