proposition: Theorem nth_size : forall {A:Type}(p:nat)(v:t A p)(n:nat), vector_nth n v = None <-> p <= n.
proof: Proof. induction v;simpl; auto. - intro n; case n; simpl; split; auto with arith. - intro n0;case n0;simpl;split. + discriminate. + inversion 1. + case (IHv n1);auto with arith. + case (IHv n1);auto with arith. Qed.
imports: Vector