proposition: Lemma pm_distrib_left : forall dim m1 m2 (m3:matrix dim), prod_matrix _ (sum_matrix _ m1 m2) m3 ==m sum_matrix _ (prod_matrix dim m1 m3) (prod_matrix _ m2 m3).
proof: Proof. fix pm_distrib_left 1. intros [|dim]. simpl. intros. apply mult_distrib_left. simpl matrix. intros [a1 [r1 [c1 m1]]] [a2 [r2 [c2 m2]]] [a3 [r3 [c3 m3]]]. simpl. refine (conj _ (conj _ (conj _ _ ))). 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 psv_distrib_left. rewrite prm_distrib_left. repeat rewrite sum_vector_assoc. rewrite <- (sum_vector_assoc _ (prod_scal_vec dim a2 r3)). rewrite (sum_vector_comm _ (prod_scal_vec dim a2 r3)). rewrite sum_vector_assoc. reflexivity. repeat rewrite psv_distrib_right. repeat rewrite pmc_distrib_left. repeat rewrite sum_vector_assoc. rewrite <- (sum_vector_assoc _ (prod_scal_vec dim a3 c2)). rewrite (sum_vector_comm _ (prod_scal_vec dim a3 c2)). rewrite sum_vector_assoc. repeat rewrite pcr_distrib_left. repeat rewrite pm_distrib_left. repeat rewrite sum_matrix_assoc. reflexivity. rewrite <- sum_matrix_assoc. rewrite <- (sum_matrix_comm _ ((prod_col_row dim c2 r3))). rewrite sum_matrix_assoc. rewrite (sum_vector_comm _ c1). rewrite pcr_distrib_left. rewrite pm_distrib_left. repeat rewrite sum_matrix_assoc. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)