proposition: Lemma Vnth_app : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) i (h : i < n1+n2), Vnth (Vapp v1 v2) h = match le_gt_dec n1 i with | left p => Vnth v2 (Vnth_app_aux h p) | right p => Vnth v1 p end.
proof: Proof. induction v1; intros. simpl. apply Vnth_eq. lia. destruct i. refl. simpl le_gt_dec. ded (IHv1 _ v2 i (NatCompat.lt_S_n h0)). revert H. case (le_gt_dec n i); simpl; intros. trans (Vnth v2 (Vnth_app_aux (NatCompat.lt_S_n h0) l)). hyp. apply Vnth_eq. lia. trans (Vnth v1 g). hyp. apply Vnth_eq. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)