proposition: Lemma Vnth_add : forall n (v : vector A n) x i (h : i < S n), Vnth (Vadd v x) h = match eq_nat_dec i n with | left _ => x | right n => Vnth v (Vnth_add_aux h n) end.
proof: Proof. induction v; intros x i hi; simpl Vadd. destruct (eq_nat_dec i 0). apply Vnth_cons_head. hyp. lia. destruct (eq_nat_dec i (S n)). subst. rewrite Vnth_cons. destruct (lt_ge_dec 0 (S n)). 2: lia. rewrite IHv. destruct (eq_nat_dec (S n - 1) n). refl. lia. rename h into y. rewrite Vnth_cons. destruct (lt_ge_dec 0 i). rewrite IHv. destruct (eq_nat_dec (i-1) n). lia. rewrite Vnth_cons. destruct (lt_ge_dec 0 i). 2: lia. apply Vnth_eq. refl. sym. apply Vnth_cons_head. lia. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)