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. fix pcr_distrib_right 1. intros [|dim]. simpl. intros. apply mult_distrib_right. simpl vector. intros [a1 c1] [a2 c2] [a r]. simpl. refine (conj _ (conj _ (conj _ _ ))). apply mult_distrib_right. apply psv_distrib_right. apply psv_distrib_left. apply pcr_distrib_right. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)