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