proposition: Theorem list_nth_pad_sub : ∀ i s (v : α) cl d, (s ≤ i)%nat → List.nth i (list_pad s v cl) d = List.nth (i - s) cl d.
proof: Proof. intros i s v cl d Hsi. revert i Hsi. induction s; intros; [ rewrite Nat.sub_0_r; reflexivity | simpl ]. destruct i; [ exfalso; revert Hsi; apply Nat.nle_succ_0 | idtac ]. apply le_S_n in Hsi. rewrite Nat.sub_succ. apply IHs; assumption. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation