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. fix sum_matrix_assoc 1. intros [|dim]. simpl; apply plus_assoc. simpl matrix. intros [a1 [r1 [c1 m1]]] [a2 [r2 [c2 m2]]] [a3 [r3 [c3 m3]]]. simpl. refine (conj _ (conj _ (conj _ _ ))). apply plus_assoc. apply sum_vector_assoc. apply sum_vector_assoc. apply sum_matrix_assoc. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)