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