proposition: Lemma Vremove_last_add : forall n (v : vector A n) x, Vremove_last (Vadd v x) = v.
proof: Proof. intros n v x. apply Veq_nth. intros i h. rewrite Vnth_remove_last, Vnth_add. destruct (eq_nat_dec i n). lia. apply Vnth_eq. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)