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