proposition: Lemma psm_comm : forall dim (a1 a2:A) (v:matrix dim), prod_scal_mat _ a1 (prod_scal_mat _ a2 v) ==m prod_scal_mat _ a2 (prod_scal_mat _ a1 v).
proof: Proof. apply psm_comm with (eq:=eq) (mult:=mult). apply eq_Equivalence. intros;ring. intros;ring. apply mult_morph. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)