proposition: Lemma VSn_add : forall n (v : vector A (S n)), v = Vadd (Vremove_last v) (Vlast (Vhead v) v).
proof: Proof. intros n v. apply VSn_add_default. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)