proposition: Lemma mint_eval_cons : forall n k val c_hd c_tl a_hd (a_tl : vector (vector mat k) n), mint_eval val (mkMatrixInt (c_hd [+] c_tl) (combine_matrices (Vcons a_hd a_tl))) =v mint_eval val (mkMatrixInt c_hd a_hd) [+] mint_eval val (mkMatrixInt c_tl (combine_matrices a_tl)).
proof: Proof. intros. unfold mint_eval. simpl. set (vali := Vbuild (A := vec) (fun i (_ : i < k) => dom2vec (val i))). rewrite combine_matrices_cons. autorewrite with arith. rewrite <- !vector_plus_assoc. apply vector_plus_mor. refl. rewrite vector_plus_assoc, (vector_plus_comm _ c_tl), <- vector_plus_assoc. apply vector_plus_mor. refl. apply add_vectors_split. intros. rewrite !Vnth_map2, vector_plus_comm. apply mat_vec_prod_distr_mat. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)