fact: Definition Vtail_total (A : Type) (n : nat) (v : t A n) : t A (pred n):= match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with | Vector.nil _ => Vector.nil A | Vector.cons _ _ n0 v0 => v0 end.
imports: Arith Vector List Extraction ZArith Compare_dec