proposition: Lemma eq_mat_sym dim : forall (v1 v2:matrix dim), v1 ==m v2 -> v2 ==m v1.
proof: Proof. apply eq_mat_sym with (eq:=eq). apply eq_Equivalence. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)