proposition: Lemma combine_matrices_nil : forall i, combine_matrices Vnil = Vconst (@zero_matrix dim dim) i.
proof: Proof. intros. apply Veq_nth. intros. unfold combine_matrices. rewrite Vnth_const, Vbuild_nth. trivial. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)