proposition: Lemma sum_matrix_comm : forall dim m1 m2, sum_matrix dim m1 m2 ==m sum_matrix dim m2 m1.
proof: Proof. fix sum_matrix_comm 1. intros [|dim]. simpl; apply plus_comm. simpl matrix. intros [a1 [r1 [c1 m1]]] [a2 [r2 [c2 m2]]]. simpl. refine (conj _ (conj _ (conj _ _ ))). apply plus_comm. apply sum_vector_comm. apply sum_vector_comm. apply sum_matrix_comm. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)