proposition: Lemma add_vectors_perm n i v v' (vs : vector (vec n) i) : add_vectors (Vcons v (Vcons v' vs)) =v add_vectors (Vcons v' (Vcons v vs)).
proof: Proof. rewrite !add_vectors_cons, !vector_plus_assoc, (vector_plus_comm v v'). refl. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)