proposition: Lemma sum_matrix_comm : forall dim m1 m2, sum_matrix dim m1 m2 ==m sum_matrix dim m2 m1.
proof: Proof. apply sum_matrix_comm with (eq:=eq) (plus:=plus). intros;ring. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)