proposition: Lemma add_vectors_nth n k : forall (vs : vector (vec n) k) i (ip : i < n), Vnth (add_vectors vs) ip =A= Vfold_left_rev Aplus A0 (Vmap (fun v => Vnth v ip) vs).
proof: Proof. induction vs; simpl; intros. unfold add_vectors, zero_vec; simpl. rewrite Vnth_const. refl. rewrite (Vforall2_elim_nth (R:=eqA)). 2: rewrite add_vectors_cons; refl. rewrite vector_plus_nth, IHvs, Aplus_comm. refl. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)