proposition: Lemma rev_nth : forall l d n, n < length l -> nth n (rev l) d = nth (length l - S n) l d.
proof: Proof. intros l d; induction l as [|a l IHl] using rev_ind; [easy|]. rewrite rev_app_distr, app_length, Nat.add_comm. cbn. intros [|n]. - now rewrite Nat.sub_0_r, nth_middle. - intros Hn %Nat.succ_lt_mono. rewrite (IHl _ Hn), app_nth1; [reflexivity|]. apply Nat.sub_lt; [assumption|apply Nat.lt_0_succ]. Qed.
imports: PeanoNat