This addresses #33 (closed)
I did not include any of the map lemmas, since we have versions of them for fmap (notation <$>).
map
fmap
<$>
I find the following lemma pretty weird:
Lemma vec_to_list_take_drop {A n} (i : fin n) (v : vec A n) : vtake i v ++ vdrop i v = v. Proof. by rewrite vec_to_list_take, vec_to_list_drop, take_drop. Qed.
It involves implicit coercions to list, and it uses the append on lists.
Unless @lepigre has a good reason for it, I rather not include it.
