proposition: Lemma Vcons_nth : forall n (v : vector A n) i k (h1 : i<n) (h2 : S i + k <= n), Vcons (Vnth v h1) (Vsub v h2) = Vsub v (Vcons_nth_aux1 h1 h2).
proof: Proof. intros. apply Veq_nth; intros. destruct i0; simpl; repeat rewrite Vnth_sub; apply Vnth_eq; lia. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)