proposition: Lemma combine_matrices_cons : forall k n v (vs : vector (vector mat k) n), combine_matrices (Vcons v vs) = Vmap2 (@mat_plus _ _) (combine_matrices vs) v.
proof: Proof. intros. apply Veq_nth. intros. unfold combine_matrices, add_matrices. simpl. rewrite Vnth_map2, !Vbuild_nth. refl. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)