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