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