proposition: Lemma add_vectors_zero n k : forall v : vector (vec n) k, Vforall (fun v => v =v zero_vec n) v -> add_vectors v =v zero_vec n.
proof: Proof. induction v. refl. rewrite add_vectors_cons. simpl. intuition. rewrite H0, vector_plus_zero_l. hyp. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)