proposition: Lemma nth_app_r {A} (a : A) {n} (l l' : list A) : length l <= n -> nth n (l @ l') a = nth (n - length l) l' a.
proof: Proof. revert l l' n; induction l; intros; auto. simpl in H. depelim H; auto. destruct n; simpl in H. depelim H. simpl; apply IHl; lia. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia