proposition: Lemma psm_distrib_right : forall dim c (r1 r2:matrix dim), prod_scal_mat _ c (sum_matrix _ r1 r2) ==m sum_matrix _ (prod_scal_mat dim c r1) (prod_scal_mat _ c r2).
proof: Proof. fix psm_distrib_right 1. intros [|dim]. simpl. intros. apply mult_distrib_right. simpl matrix. intros c [a1 [ r1 [c1 m1]]] [a2 [r2 [c2 m2]]]. simpl. refine (conj _ (conj _ (conj _ _ ))). apply mult_distrib_right. apply psv_distrib_right. apply psv_distrib_right. apply psm_distrib_right. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)