proposition: Lemma eq_mat_sym dim : forall (v1 v2:matrix dim), v1 ==m v2 -> v2 ==m v1.
proof: Proof. induction dim. simpl;intros. symmetry;assumption. simpl;intros [a1 [r1 [c1 m1]]] [a2 [r2 [c2 m2]]] [a3 [r3 [c3 m3]]]. intuition try symmetry;auto. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)