fact: Definition combine_matrices n k (v : vector (vector mat k) n) := Vbuild (fun i ip => add_matrices (Vmap (fun v => Vnth v ip) v)).
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)