proposition: Lemma to_list_nth_order A n (v : t A n) p (H : p < n) d: nth_order v H = List.nth p (to_list v) d.
proof: Proof. unfold nth_order. revert p H. induction v as [|a n v IH]. - intros p H. destruct (Nat.nlt_0_r p H). - intros [|p] ?; [ reflexivity | apply IH ]. Qed.
imports: VectorDef PeanoNat Eqdep_dec