fact: Definition tailOpt(A : Set)(n : nat)(v : Vector.t A n) : option (Vector.t A (pred n)):= match v with | [] => None | Vector.cons _ _ _ v => Some v end.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation