fact: Fixpoint splitVector(A : Set)(n m : nat) : Vector.t A (n + m) -> (Vector.t A n * Vector.t A m) := match n with | 0 => fun (v : Vector.t A (O + m)) => (@Vector.nil A, v) | S n' => fun (v : Vector.t A (S n' + m)) => let (v1, v2) := splitVector _ _ (Vector.tl v) in (Vector.cons _ (Vector.hd v) _ v1, v2) end.
imports: Bvector List Arith