proposition: Lemma eq_vec_sym dim : forall (v1 v2:vector dim), v1 ==v v2 -> v2 ==v v1.
proof: Proof. induction dim. simpl;intros. symmetry;assumption. simpl;intros [a1 v1] [a2 v2] [a3 v3]. intuition. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)