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