proposition: Lemma pmc_distrib_left : forall dim m1 m2 (c:vector dim), prod_mat_col _ (sum_matrix _ m1 m2) c ==v sum_vector _ (prod_mat_col dim m1 c) (prod_mat_col _ m2 c).
proof: Proof. fix pmc_distrib_left 1. intros [|dim]. simpl. intros. apply mult_distrib_left. simpl vector;simpl matrix. intros [a1 [r1 [c1 m1]]] [a2 [r2 [c2 m2]]] [a3 c3]. simpl. constructor. repeat rewrite mult_distrib_left. rewrite prc_distrib_left. repeat rewrite plus_assoc. rewrite <- (plus_assoc (mult a2 a3)). rewrite (plus_comm (mult a2 a3)). rewrite plus_assoc. reflexivity. rewrite pmc_distrib_left. rewrite psv_distrib_right. repeat rewrite sum_vector_assoc. rewrite <- (sum_vector_assoc _ (prod_scal_vec _ a3 c2)). rewrite (sum_vector_comm _(prod_scal_vec _ a3 c2)). rewrite sum_vector_assoc. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)