proposition: Theorem list_nth_pad_lt : ∀ i s (v : α) cl d, (i < s)%nat → List.nth i (list_pad s v cl) d = v.
proof: Proof. intros i s v cl d His. revert i His. induction s; intros. exfalso; revert His; apply lt_n_0. simpl. destruct i; [ reflexivity | idtac ]. apply IHs, lt_S_n; assumption. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation