proposition: Lemma pcr_distrib_right : forall dim c (r1 r2:vector dim), prod_col_row _ c (sum_vector _ r1 r2) ==m sum_matrix _ (prod_col_row dim c r1) (prod_col_row _ c r2).
proof: Proof. apply pcr_distrib_right with (eq:=eq) (plus:=plus) (mult:=mult). intros;ring. intros;ring. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)