proposition: Lemma Vnth_cons_tail : forall x n (v : vector A n) i (h1:i<S n) (h2:i>0), Vnth (Vcons x v) h1 = Vnth v (Vnth_cons_tail_aux h1 h2).
proof: Proof. intros. simpl. destruct i. lia. apply Vnth_eq. lia. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)