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