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. fix psm_distrib_left 1. intros [|dim]. simpl. intros. apply mult_distrib_left. simpl matrix. intros c1 c2 [a [r [l m]]]. simpl. refine (conj _ (conj _ (conj _ _ ))). apply mult_distrib_left. apply psv_distrib_left. apply psv_distrib_left. apply psm_distrib_left. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)