proposition: Lemma Veq_app_aux : forall n (v : vector A n) i (h1 : 0 + i <= n) (h2 : i + (n - i) <= n) (e : i + (n - i) = n), v = Vcast (Vapp (Vsub v h1) (Vsub v h2)) e.
proof: Proof. induction v; intros. apply Veq_nth; intros. lia. destruct i; simpl in *; [rewrite Vcast_refl | rewrite Vcast_cons]; f_equal; rewrite !Vsub_cons. apply Veq_nth; intros; rewrite Vnth_sub; apply Vnth_eq. refl. apply IHv. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)