proposition: Lemma add_vectors_cons n i (a : vec n) (v : vector (vec n) i) : add_vectors (Vcons a v) =v a [+] add_vectors v.
proof: Proof. unfold add_vectors. simpl. rewrite vector_plus_comm. refl. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)