proposition: Lemma VSn_add_default : forall x n (v : vector A (S n)), v = Vadd (Vremove_last v) (Vlast x v).
proof: Proof. intros x n v. apply Veq_nth. intros i h. destruct (lt_dec i n). rewrite Vnth_addl with (H2:=l), Vnth_remove_last. apply Vnth_eq. refl. rewrite Vnth_addr. 2: lia. assert (e : i=n). lia. subst i. rewrite Vlast_nth with (h:=h). refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)