proposition: Lemma Vnth_sub : forall k n (v : vector A n) i (h : i+k<=n) j (p : j<k), Vnth (Vsub v h) p = Vnth v (Vnth_sub_aux h p).
proof: Proof. induction k; intros. lia. simpl. destruct j. apply Vnth_eq. lia. rewrite IHk. apply Vnth_eq. lia. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)