proposition: Lemma Vsub_cons : forall x i k n (v : vector A n) (h : S i + k <= S n), Vsub (Vcons x v) h = Vsub v (Vsub_cons_aux h).
proof: Proof. intros. apply Veq_nth; intros. rewrite !Vnth_sub. simpl. apply Vnth_eq. lia. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)