proposition: Lemma psm_distrib_left : forall dim c1 c2 (m:matrix dim), prod_scal_mat _ (plus c1 c2) m ==m sum_matrix _ (prod_scal_mat dim c1 m) (prod_scal_mat _ c2 m).
proof: Proof. apply psm_distrib_left with (eq:=eq) (plus:=plus) (mult:=mult). intros;ring. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)